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

ANNOUNCE

author | kleing |

Sat Apr 17 14:57:50 2004 +0200 (2004-04-17) | |

changeset 14616 | b167b1b848d8 |

parent 14614 | 196ff8d245bf |

child 14624 | 9b3397a848c3 |

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

added sydney mirror

1 Subject: Announcing Isabelle2004

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

4 Isabelle2004 is now available.

6 This release provides many improvements and a few substantial advances over

7 Isabelle2003. The most prominent highlights of Isabelle2004 are as follows

8 (see the NEWS of the distribution for more details):

11 * New theory Ring_and_Field with over 250 basic numerical laws,

12 all proved in axiomatic type classes for semirings, rings and fields.

14 * Type "rat" of the rational numbers available in HOL-Complex.

16 * New locale "ring" for non-commutative rings in HOL-Algebra.

18 * New theory of matrices with an application to linear programming in

19 HOL-Matrix.

21 * Improved locales (named proof contexts), instantiation of locales.

23 * Improved handling of linear and partial orders in simplifier.

25 * New "specification" command for definition by specification.

27 * New Isar command "finalconsts" prevents constants being given a definition

28 later.

30 * Command "arith" now generates counterexamples for reals as well.

32 * New "quickcheck" command to search for counterexamples of executable goals.

33 (see HOL/ex/Quickcheck_Examples.thy)

35 * New "refute" command to search for finite countermodels of goals.

36 (see HOL/ex/Refute_Examples.thy)

38 * Presentation and x-symbol enhancements, greek letters and sub/superscripts

39 allowed in identifiers.

42 You may get Isabelle2004 from the following mirror sites:

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

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

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

48 Gerwin Klein

49 Tobias Nipkow

50 Larry Paulson