*** empty log message ***

--- a/NEWS	Mon Sep 06 18:18:09 1999 +0200
+++ b/NEWS	Mon Sep 06 18:18:23 1999 +0200
@@ -102,6 +102,7 @@
 
 * function bind_thms stores lists of theorems (cf. bind_thm);
 
+* new shorthand tactics ftac, eatac, datac, fatac
 
 *** HOL ***
 
@@ -206,6 +207,9 @@
 HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
 time;
 
+* HOL: new tactic smp_tac: int -> int -> tactic, which applies spec several
+  times and then mp
+
 
 *** LK ***