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

ANNOUNCE

author | wenzelm |

Thu Feb 28 21:30:03 2002 +0100 (2002-02-28) | |

changeset 12983 | 7d13480ee668 |

parent 12964 | 2ac9265b2cd5 |

child 12993 | 1b76cc7ffef7 |

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

more stuff;

2 Subject: Announcing Isabelle2002

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

5 Isabelle2002 is now available.

7 In this release many important aspects of Isabelle have been reworked,

8 to improve robustness and usability. This occasionally causes

9 incompatibility with earlier versions.

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

12 NEWS of the distribution for more details).

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

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

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

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

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

20 (by Stefan Berghofer).

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

23 theory development; additional support for rename/merge

24 operations, and type-inference for structured specifications

25 (by Markus Wenzel).

27 * Pure/Isar: streamlined induction proof patterns

28 (by Markus Wenzel).

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

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

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

34 improvements of tuple and record types; new definite description

35 operator; keep Hilbert's choice out of basic theories.

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

38 (by David von Oheimb and Norbert Schirmer).

40 * HOL/Hoare_Parallel: large application concerning verification of

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

42 (by Leonor Prensa Nieto).

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

45 (by Florian Kammüller).

47 * HOL/IMP: new proofs in Isar format

48 (by Gerwin Klein).

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

51 (by Sidi O Ehmety).

53 * System: improvements and simplifications of document preparation

54 (by Markus Wenzel).

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

57 larger heap size of applications.

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

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

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

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

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

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