[isabelle-dev] NEWS

[Johannes Hoelzl]

* 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>