[isabelle] Call for real limit problems


I'm currently working on some more automation for real limits. For that
purpose, I'd like to collect some âreal-world problemsâ from Isabelle users.

I am looking for problems involving the limit of functions of type "real
â real" built from arithmetic (+-*/^), powr, sqrt, root, ln, exp, abs,
min, max as well as sin, cos, tan at finite points. Real parameters
(i.e. free variables of type "real") are also allowed.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.