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? Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
