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

ANNOUNCE

author | wenzelm |

Thu Mar 07 23:41:30 2002 +0100 (2002-03-07) | |

changeset 13043 | ad1828b479b7 |

parent 13042 | d8a345d9e067 |

child 13045 | 1db0bdda1d32 |

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

renamed nat_number_of to nat_number (avoid clash with separate theorem);

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

8 reached a mature state; the core engine is able to record full proof

9 terms; many aspects of the library have been reworked; several

10 substantial case studies have been added. Some changes may cause

11 incompatibility with earlier versions, but improve accessibility of

12 Isabelle for new users.

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

15 NEWS of the distribution for more details).

17 * The Isabelle/HOL tutorial is to be published as LNCS 2283;

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

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

21 * Pure: explicit proof terms for all internal inferences;

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

23 (by Stefan Berghofer).

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

26 theory development; additional support for rename/merge

27 operations, and type-inference for structured specifications

28 (by Markus Wenzel).

30 * Pure/Isar: streamlined cases/induction proof patterns

31 (by Markus Wenzel).

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

34 code, using the ML run-time environment

35 (by Stefan Berghofer).

37 * HOL/library: numerals on all number types; several improvements of

38 tuple and record types; new definite description operator; keep

39 Hilbert's epsilon (Axiom of Choice) out of basic theories

40 (by Stefan Berghofer, Larry Paulson, Markus Wenzel).

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

43 (by David von Oheimb and Norbert Schirmer).

45 * HOL/HoareParallel: large application concerning verification of

46 parallel imperative programs (Owicki-Gries method, Rely-Guarantee

47 method, examples of garbage collection, mutual exclusion)

48 (by Leonor Prensa Nieto).

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

51 (by Florian Kammueller).

53 * HOL/IMP: several new proofs in Isar format

54 (by Gerwin Klein).

56 * HOL/MicroJava: exception handling on the bytecode level

57 (by Gerwin Klein).

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

60 (by Sidi O Ehmety).

62 * System: improvements and simplifications of document preparation

63 (by Markus Wenzel).

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

66 larger heap size of applications; support for MacOS X (Poly/ML and

67 SML/NJ).

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

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

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

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

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