I'm happy to have whatever you deem useful moved to the library. Manuel
On 03/07/2021 13:04, Lawrence Paulson wrote: > Yesterday I renamed arg -> Arg along with most of the arg_ theorems (though > we still have arg_unique and Arg_unique). > > I noticed some useful-looking basic lemmas about Arg in > Stirling_Formula/Gamma_Asymptotics.thy (added to the AFP by Manuel in 2016) > that we might bring into the libraries. Any comments? > > Larry > >> On 25 Jun 2021, at 21:28, Lawrence Paulson <[email protected]> wrote: >> >> I’ve just noticed that we define both arg and Arg, the latter in >> Complex_Transcendental. >> >> The definitions are different but arg z = Arg z holds unconditionally. It >> looks like a historical accident, maybe arg was introduced in the 1990s and >> forgotten about. >> >> Interestingly enough, arg is used far more despite there being almost >> nothing proved about it. Some lemmas are proved in >> Complex_Geometry/More_Complex.thy, and many occurrences of “arg” are simply >> variables. >> >> This is a mess. Any suggestions? Maybe Arg could (temporarily) be made an >> abbreviation for arg. Arg is the usual of the function (principal value of >> the argument). >> >> Larry >> >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
