# HG changeset patch
# User oheimb
# Date 936634703 -7200
# Node ID 44b333fb5b8049494efef677dae00a890bf7c502
# Parent  95a4af0e10a7f0bc82deca827b1b1c6cff1a0ffd
*** empty log message ***

diff -r 95a4af0e10a7 -r 44b333fb5b80 NEWS
--- 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 ***