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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
