NEWS
changeset 7492 44b333fb5b80
parent 7450 e329ca03fd00
child 7593 6bc8fa8b4b24
     1.1 --- a/NEWS	Mon Sep 06 18:18:09 1999 +0200
     1.2 +++ b/NEWS	Mon Sep 06 18:18:23 1999 +0200
     1.3 @@ -102,6 +102,7 @@
     1.4  
     1.5  * function bind_thms stores lists of theorems (cf. bind_thm);
     1.6  
     1.7 +* new shorthand tactics ftac, eatac, datac, fatac
     1.8  
     1.9  *** HOL ***
    1.10  
    1.11 @@ -206,6 +207,9 @@
    1.12  HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
    1.13  time;
    1.14  
    1.15 +* HOL: new tactic smp_tac: int -> int -> tactic, which applies spec several
    1.16 +  times and then mp
    1.17 +
    1.18  
    1.19  *** LK ***
    1.20