--- a/NEWS Fri Mar 07 09:56:55 1997 +0100
+++ b/NEWS Fri Mar 07 10:19:24 1997 +0100
@@ -14,12 +14,12 @@
* HOLCF changes: derived all rules and arities
+ axiomatic type classes instead of classes
+ typedef instead of faking type definitions
- + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
+ + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
+ new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
+ eliminated the types void, one, tr
+ use unit lift and bool lift (with translations) instead of one and tr
+ eliminated blift from Lift3.thy (use Def instead of blift)
- all eliminated rules are derivd as theorems --> no visible changes
+ all eliminated rules are derived as theorems --> no visible changes
* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
@@ -28,16 +28,19 @@
functions setsolver and addsolver have been renamed to setSolver and
addSolver. added safe_asm_full_simp_tac.
-* classical reasoner: little changes in semantics of addafter (now:
-addaltern), renamed setwrapper to setWrapper, addwrapper to addWrapper
+* 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 addwrapper to addWrapper;
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)
-possible COULD MAKE EXISTING PROOFS FAIL; in case of problems with
-unstable old proofs: use unsafe_addss and unsafe_auto_tac
+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: primrec now also works with type nat;
@@ -55,7 +58,7 @@
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
+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;
@@ -148,7 +151,7 @@
New in Isabelle94-4
-------------------
-* greatly space requirements;
+* greatly reduced space requirements;
* theory files (.thy) no longer require \...\ escapes at line breaks;