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

ANNOUNCE

author | berghofe |

Thu Apr 21 19:12:03 2005 +0200 (2005-04-21) | |

changeset 15797 | a63605582573 |

parent 14624 | 9b3397a848c3 |

child 17544 | 929d157d4369 |

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

- Eliminated nodup_vars check.

- Unification and matching functions now check types of term variables / sorts

of type variables when applying a substitution.

- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list

as argument, to allow for proper instantiation of theorems containing

type variables with same name but different sorts.

- Unification and matching functions now check types of term variables / sorts

of type variables when applying a substitution.

- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list

as argument, to allow for proper instantiation of theorems containing

type variables with same name but different sorts.

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 image HOL4 with imported library from HOL4 system on top of

12 HOL-Complex (about 2500 additional theorems).

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

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

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

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

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

22 HOL-Matrix.

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

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

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

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

31 later.

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

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

36 (see HOL/ex/Quickcheck_Examples.thy)

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

39 (see HOL/ex/Refute_Examples.thy)

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

42 allowed in identifiers.

45 You may get Isabelle2004 from the following mirror sites:

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

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

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

51 Gerwin Klein

52 Tobias Nipkow

53 Larry Paulson