<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><font size="+1">Note that I set up something to deal with this
(periodicity of sin/cos/etc) in HOL-Library.Periodic_Fun.</font></p>
<p><font size="+1">I have some plans for making a simproc to deal
with the obvious cases automatically, but so far I have not
found a suitable student to implement it.</font></p>
<p><font size="+1">Manuel<br>
</font></p>
<div class="moz-cite-prefix">On 19/02/2021 14:51, Tobias Nipkow
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:31767d10-0d7e-6cb8-238d-b6ec06510975@in.tum.de">
<br>
<br>
On 19/02/2021 13:35, Lawrence Paulson wrote:
<br>
<blockquote type="cite">It’s common for AFP entries to include
theories with names such as T_extras, extending some theory T.
Sometimes they look interesting. The entry Complex_Geometry has
quite a few of such theories. For example, More_Transcendental
contains a lot of facts about sines and cosines, such as the
following:
<br>
<br>
lemma cos_periodic_int [simp]:
<br>
fixes i :: int
<br>
shows "cos (x + i * (2 * pi)) = cos x”
<br>
<br>
Should we from time to time seek to import some of this
material?
<br>
</blockquote>
<br>
If you can spare the time, by all means.
<br>
<br>
Tobias
<br>
<br>
<blockquote type="cite">Larry
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
<br>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
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://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>