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

[Lawrence Paulson]

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