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

ANNOUNCE

author | paulson |

Fri Mar 01 13:07:25 2002 +0100 (2002-03-01) | |

changeset 12993 | 1b76cc7ffef7 |

parent 12983 | 7d13480ee668 |

child 12995 | d9da3015aab4 |

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

lcp's try

2 Subject: Announcing Isabelle2002

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

5 Isabelle2002 is now available.

7 This release provides major improvements. The Isar language has reached a

8 mature state; the treatment of numerals has been streamlined; several

9 substantial case studies have been added. This occasionally causes

10 incompatibility with earlier versions.

12 The most prominent highlights of Isabelle2002 are as follows (see the

13 NEWS of the distribution for more details).

15 * The Isabelle/HOL tutorial has been published as LNCS 2283;

16 Isabelle2002 is the official version to go along with that book

17 (by Tobias Nipkow, Larry Paulson, Markus Wenzel).

19 * Pure: explicit proof terms for all internal inferences:

20 object-logics, proof tools etc. will benefit automatically

21 (by Stefan Berghofer).

23 * Pure/Isar: proper integration of the locale package for modular

24 theory development; additional support for rename/merge

25 operations, and type-inference for structured specifications

26 (by Markus Wenzel).

28 * Pure/Isar: streamlined induction proof patterns

29 (by Markus Wenzel).

31 * Pure/HOL: infrastructure for generating functional and relational

32 code, using the ML run-time environment (by Stefan Berghofer).

34 * HOL/library: numerals on all number types; several

35 improvements of tuple and record types; new definite description

36 operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.

38 * HOL/Bali: large application concerning formal treatment of Java.

39 (by David von Oheimb and Norbert Schirmer).

41 * HOL/Hoare_Parallel: large application concerning verification of

42 parallel imperative programs (Owicki-Gries method etc.)

43 (by Leonor Prensa Nieto).

45 * HOL/GroupTheory: group theory examples including Sylow's theorem

46 (by Florian Kammüller).

48 * HOL/IMP: new proofs in Isar format

49 (by Gerwin Klein).

51 * ZF/UNITY: typeless version of Chandy and Misra's formalism

52 (by Sidi O Ehmety).

54 * System: improvements and simplifications of document preparation

55 (by Markus Wenzel).

57 * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting

58 larger heap size of applications.

60 * System: support for MacOS X (for Poly/ML and SML/NJ).

63 You may get Isabelle2002 from any of the following mirror sites:

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

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

67 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html

68 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html