--- a/NEWS Fri Sep 26 10:21:14 1997 +0200
+++ b/NEWS Mon Sep 29 11:28:23 1997 +0200
@@ -29,6 +29,8 @@
new tactics that use classical reasoning to simplify a subgoal
without splitting it into several subgoals;
+* Safe_tac: like safe_tac but uses the default claset;
+
*** Simplifier ***
@@ -65,6 +67,11 @@
adm (%x. P (t x)), where P is chainfinite and t continuous.
+*** FOL and ZF ***
+
+* qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available. As
+ in HOL, they strip ALL and --> from proved theorems;
+
New in Isabelle94-8 (May 1997)
------------------------------