[isabelle-dev] lots of interesting lemmas in the AFP entry Complex_Geometry

[Tobias Nipkow]

On 19/02/2021 13:35, Lawrence Paulson wrote:
> 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:
> 
> lemma cos_periodic_int [simp]:
>    fixes i :: int
>    shows "cos (x + i * (2 * pi)) = cos x”
> 
> Should we from time to time seek to import some of this material?

If you can spare the time, by all means.

Tobias

> Larry
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210219/d6df17fd/attachment.bin>