# HG changeset patch
# User wenzelm
# Date 918743410 -3600
# Node ID dbb48b0744d369a481bef20a477908b16c53b836
# Parent  9d2dad7489f4a003021e9aa6cf845143cb77c7d6
tuned;
TLA update;

diff -r 9d2dad7489f4 -r dbb48b0744d3 NEWS
--- 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)