summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

ANNOUNCE

author | wenzelm |

Fri Sep 23 22:21:49 2005 +0200 (2005-09-23) | |

changeset 17609 | 5156b731ebc8 |

parent 17572 | 81fcc0029761 |

child 17684 | c98508731bd6 |

permissions | -rw-r--r-- |

Provers/cancel_sums.ML: Simplifier.inherit_bounds;

1 Subject: Announcing Isabelle2005

2 To: isabelle-users@cl.cam.ac.uk

4 Isabelle2005 is now available.

6 This release provides substantial advances over Isabelle2004, see the

7 first 1000 lines of NEWS in the distribution for more details. Some

8 notable highlights are:

10 * Interpretation of locale expressions in theories, locales, and proof

11 contexts.

13 * Substantial library improvements (HOL, HOL-Complex, HOLCF).

15 * Proof tools for transitivity reasoning.

17 * General 'find_theorems' command (by term patterns, as

18 intro/elim/simp rules etc.).

20 * Commands for generating adhoc draft documents.

22 * Support for Unicode proof documents (UTF-8).

24 * Major internal reorganizations and performance improvements.

27 You may get Isabelle2005 from the following mirror sites:

29 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/

30 Munich (Germany) http://isabelle.in.tum.de/dist/

31 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/