# HG changeset patch
# User paulson
# Date 875525303 -7200
# Node ID 6a142dab2a080e386c2423992f8774ce3173899c
# Parent  d78cf498a88c06787349ac2b61e86db4e53dc41d
Safe_tac; qed_spec_mp in FOL

diff -r d78cf498a88c -r 6a142dab2a08 NEWS
--- 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)
 ------------------------------