<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">I would also have suggested an AFP entry.</font></p>
<p>
<blockquote type="cite">
<pre wrap="">let reflect_along = new_definition
`reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;</pre>
</blockquote>
Think of it as x being the direction of a ray of light hitting a
mirror (in the shape of a hyperplane through the origin with
normal vector a) and being reflected. The result is the direction
of the reflected ray.</p>
<p>Where it belongs I cannot say; that depends on what kinds of
results are proven about it. I for one would consider this a very
‘applied’ concept (I know it from ray tracing), so unless we have
a concrete application for it, I'm not sure we need it at all.<br>
</p>
<p>Manuel<br>
</p>
<br>
<div class="moz-cite-prefix">On 2018-06-18 14:17, Lars Hupel wrote:<br>
</div>
<blockquote type="cite"
cite="mid:bb02446e-ef9b-5a39-f243-35f81adc1829@in.tum.de">
<blockquote type="cite">
<pre wrap="">So where does this material belong? Arguably not in Analysis, which is already too large.
</pre>
</blockquote>
<pre wrap="">
Why not a regular AFP entry?
Cheers
Lars
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>