summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Thu, 05 Feb 2009 15:35:06 +0100 | |

changeset 29810 | fa4ec7a7215c |

parent 29809 | df25a6b1a475 |

child 29811 | 026b0f9f579f |

Updated NEWS about approximation

--- a/NEWS Thu Feb 05 14:50:43 2009 +0100 +++ b/NEWS Thu Feb 05 15:35:06 2009 +0100 @@ -200,8 +200,10 @@ (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 -and exp are allowed. +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. * Entry point to Word library now simply named "Word". INCOMPATIBILITY.