--- a/NEWS Mon Feb 17 16:50:17 1997 +0100
+++ b/NEWS Mon Feb 17 16:50:59 1997 +0100
@@ -2,6 +2,9 @@
Isabelle NEWS -- history of user-visible changes
================================================
+New in Isabelle94-8 (??????????? 1997 FIXME)
+---------------------------------------
+
* simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
* simplifier: the solver is now split into a safe and an unsafe part.
@@ -9,21 +12,16 @@
setsolver and addsolver have been renamed to setSolver and addSolver.
added safe_asm_full_simp_tac.
-* classical reasoner: better addbefore, addafter (now: addaltern),
- setwrapper (now: setWrapper) and addwrapper (now addWrapper)
- replaced addafter by addaltern,
+* classical reasoner: little changes in semantics of addafter (now: addaltern),
+ renamed setwrapper to setWrapper, addwrapper to addWrapper
added safe wrapper (and access functions for it)
-* better combination of classical reasoner and simplifier:
+* 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
-
-
-New in Isabelle94-8 (??????????? 1997 FIXME)
----------------------------------------
+ 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
* HOL: primrec now also works with type nat;