--- a/NEWS Mon Apr 21 10:38:46 1997 +0200
+++ b/NEWS Mon Apr 21 11:19:28 1997 +0200
@@ -5,10 +5,24 @@
New in Isabelle94-8 (April 1997)
--------------------------------
-* reimplemented type inference;
+*** General Changes ***
+
+* new utilities to build / run / maintain Isabelle etc. (in parts
+still somewhat experimental); old Makefiles etc. still functional;
* INSTALL text, together with ./configure and ./build scripts;
+* reimplemented type inference for greater efficiency;
+
+* prlim command for dealing with lots of subgoals (an easier way of
+setting goals_limit);
+
+*** Syntax
+
+* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
+be used in conjunction with the Isabelle symbol font; uses the
+"symbols" syntax table;
+
* added token_translation interface (may translate name tokens in
arbitrary ways, dependent on their type (free, bound, tfree, ...) and
the current print_mode);
@@ -16,6 +30,71 @@
* token translations for modes "xterm" and "xterm_color" that display
names in bold, underline etc. or colors;
+* now supports alternative (named) syntax tables (parser and pretty
+printer); internal interface is provided by add_modesyntax(_i);
+
+* infixes may now be declared with names independent of their syntax;
+
+* added typed_print_translation (like print_translation, but may
+access type of constant);
+
+*** Classical Reasoner ***
+
+Blast_tac: a new tactic! It is often more powerful than fast_tac, but has
+some limitations. Blast_tac...
+ + ignores addss, addbefore, addafter; this restriction is intrinsic
+ + ignores elimination rules that don't have the correct format
+ (the conclusion MUST be a formula variable)
+ + ignores types, which can make HOL proofs fail
+ + rules must not require higher-order unification, e.g. apply_type in ZF
+ [message "Function Var's argument not a bound variable" relates to this]
+ + its proof strategy is more general but can actually be slower
+
+* substitution with equality assumptions no longer permutes other assumptions.
+
+* minor changes in semantics of addafter (now called addaltern); renamed
+setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
+(and access functions for it)
+
+* improved combination of classical reasoner and simplifier: new
+addss, auto_tac, functions for handling clasimpsets, ... Now, the
+simplification is safe (therefore moved to safe_step_tac) and thus
+more complete, as multiple instantiation of unknowns (with slow_tac).
+COULD MAKE EXISTING PROOFS FAIL; in case of problems with
+old proofs, use unsafe_addss and unsafe_auto_tac
+
+*** Simplifier ***
+
+* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
+
+* the solver is now split into a safe and an unsafe part.
+This should be invisible for the normal user, except that the
+functions setsolver and addsolver have been renamed to setSolver and
+addSolver. added safe_asm_full_simp_tac.
+
+* ordering on terms as parameter (used for ordered rewriting);
+added interface for simplification procedures (functions that produce *proven*
+rewrite rules on the fly, depending on current redex);
+
+*** HOL ***
+
+* patterns in case expressions allow tuple patterns as arguments to
+constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
+
+* primrec now also works with type nat;
+
+* the constant for negation has been renamed from "not" to "Not" to
+harmonize with FOL, ZF, LK, etc.
+
+* HOL/ex/LFilter theory of a corecursive "filter" functional for infinite lists
+
+* HOL/ex/Ring.thy declares cring_simp, which solves equational
+problems in commutative rings, using axiomatic type classes for + and *;
+
+* more examples in HOL/MiniML and HOL/Auth;
+
+* more default rewrite rules for quantifiers, union/intersection;
+
* HOLCF changes: derived all rules and arities
+ axiomatic type classes instead of classes
+ typedef instead of faking type definitions
@@ -26,70 +105,12 @@
+ eliminated blift from Lift3.thy (use Def instead of blift)
all eliminated rules are derived as theorems --> no visible changes
-* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
-
-* simplifier: the solver is now split into a safe and an unsafe part.
-This should be invisible for the normal user, except that the
-functions setsolver and addsolver have been renamed to setSolver and
-addSolver. added safe_asm_full_simp_tac.
-
-* classical reasoner: substitution with equality assumptions no longer
-permutes other assumptions.
-
-* classical reasoner: minor changes in semantics of addafter (now called
-addaltern); renamed setwrapper to setWrapper and compwrapper to compWrapper;
-added safe wrapper (and access functions for it)
-
-* improved combination of classical reasoner and simplifier: new
-addss, auto_tac, functions for handling clasimpsets, ... Now, the
-simplification is safe (therefore moved to safe_step_tac) and thus
-more complete, as multiple instantiation of unknowns (with slow_tac).
-COULD MAKE EXISTING PROOFS FAIL; in case of problems with
-old proofs, use unsafe_addss and unsafe_auto_tac
-
-* HOL: patterns in case expressions allow tuple patterns as arguments to
-constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
-
-* HOL: primrec now also works with type nat;
-
-* HOL: the constant for negation has been renamed from "not" to "Not" to
-harmonize with FOL, ZF, LK, etc.
-
-* new utilities to build / run / maintain Isabelle etc. (in parts
-still somewhat experimental); old Makefiles etc. still functional;
-
-* simplifier: termless order as parameter; added interface for
-simplification procedures (functions that produce *proven* rewrite
-rules on the fly, depending on current redex);
-
-* now supports alternative (named) syntax tables (parser and pretty
-printer); internal interface is provided by add_modesyntax(_i);
-
-* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
-be used in conjunction with the Isabelle symbol font; uses the
-"symbols" syntax table;
-
-* infixes may now be declared with names independent of their syntax;
-
-* added typed_print_translation (like print_translation, but may
-access type of constant);
-
-* prlim command for dealing with lots of subgoals (an easier way of
-setting goals_limit);
-
-* HOL/ex/Ring.thy declares cring_simp, which solves equational
-problems in commutative rings, using axiomatic type classes for + and *;
+*** ZF ***
* ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default
rewrite rule; this may affect some proofs. eq_cs is gone but can be put back
as ZF_cs addSIs [equalityI];
-* more examples in HOL/MiniML and HOL/Auth;
-
-* more default rewrite rules in HOL for quantifiers, union/intersection;
-
-* the NEWS file;
-
New in Isabelle94-7 (November 96)