--- a/NEWS Tue Feb 09 10:47:21 1999 +0100
+++ b/NEWS Thu Feb 11 15:30:10 1999 +0100
@@ -1,3 +1,4 @@
+
Isabelle NEWS -- history user-relevant changes
==============================================
@@ -6,16 +7,17 @@
*** Overview of INCOMPATIBILITIES (see below for more details) ***
-* HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
+* HOL: Removed the obsolete syntax "Compl A"; use -A for set
+complement;
-* HOL: the predicate "inj" is now defined by translation to "inj_on"
+* HOL: the predicate "inj" is now defined by translation to "inj_on";
-* ZF: The con_defs part of an inductive definition may no longer refer to
- constants declared in the same theory;
+* ZF: The con_defs part of an inductive definition may no longer refer
+to constants declared in the same theory;
-* HOL, ZF: the function mk_cases, generated by the inductive definition
- package, has lost an argument. To simplify its result, it uses the default
- simpset instead of a supplied list of theorems.
+* HOL, ZF: the function mk_cases, generated by the inductive
+definition package, has lost an argument. To simplify its result, it
+uses the default simpset instead of a supplied list of theorems.
*** Proof tools ***
@@ -30,8 +32,8 @@
* in locales, the "assumes" and "defines" parts may be omitted if empty;
-* new print_mode "xsymbols" for extended symbol support
- (e.g. genuiene long arrows);
+* new print_mode "xsymbols" for extended symbol support (e.g. genuine
+long arrows);
* path element specification '~~' refers to '$ISABELLE_HOME';
@@ -56,6 +58,7 @@
NB: At the moment, these decision procedures do not cope with mixed nat/int
formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'.
+
*** Internal programming interfaces ***
* tuned current_goals_markers semantics: begin / end goal avoids
@@ -66,27 +69,34 @@
uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
string -> unit if you really want to output text without newline;
+* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
+-- avoids syntactic ambiguities and treats state, transition, and
+temporal levels more uniformly; introduces INCOMPATIBILITIES due to
+changed syntax and (many) tactics;
+
*** ZF ***
* new primrec section allows primitive recursive functions to be given
- directly (as in HOL) over datatypes and the natural numbers;
+directly (as in HOL) over datatypes and the natural numbers;
-* new tactics induct_tac and exhaust_tac for induction (or case analysis)
- over datatypes and the natural numbers;
+* new tactics induct_tac and exhaust_tac for induction (or case
+analysis) over datatypes and the natural numbers;
* the datatype declaration of type T now defines the recursor T_rec;
* simplification automatically does freeness reasoning for datatype
- constructors;
+constructors;
-* automatic type-inference, with AddTCs command to insert new type-checking
- rules;
+* automatic type-inference, with AddTCs command to insert new
+type-checking rules;
-* datatype introduction rules are now added as Safe Introduction rules to
- the claset;
+* datatype introduction rules are now added as Safe Introduction rules
+to the claset;
-* The syntax "if P then x else y" is now available in addition to if(P,x,y).
+* the syntax "if P then x else y" is now available in addition to
+if(P,x,y);
+
New in Isabelle98-1 (October 1998)