--- a/NEWS Wed Mar 05 13:40:41 1997 +0100
+++ b/NEWS Wed Mar 05 14:19:34 1997 +0100
@@ -24,20 +24,20 @@
* 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.
+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: little changes in semantics of addafter (now: addaltern),
- renamed setwrapper to setWrapper, addwrapper to addWrapper
- added safe wrapper (and access functions for it)
+* 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)
-* 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
+* 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
* HOL: primrec now also works with type nat;
@@ -81,6 +81,7 @@
* the NEWS file;
+
New in Isabelle94-7 (November 96)
---------------------------------