* Theory "Reflection" now resides in HOL/Library. Common reflection examples (Cooper, MIR, Ferrack, Approximation) now in distinct session directory HOL/Reflection. Here Approximation provides the new proof method "approximation". It proves formulas on real values by using interval arithmetic. In the formulas are also the transcendental functions sin, cos, tan, atan, ln, exp and the constant pi are allowed. For examples see src/HOL/ex/ApproximationEx.thy. To reach this the Leibnitz's Series for Pi and the arcus tangens and logarithm series is now proved in Isabelle.
-- Johannes H?lzl Homepage: http://www.in.tum.de/~hoelzl/ PGP Key: http://www.in.tum.de/~hoelzl/hoelzl_in_tum_de.pgp -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 194 bytes Desc: Dies ist ein digital signierter Nachrichtenteil URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090205/46c903cb/attachment.pgp>
