stac
authorpaulson
Thu Aug 13 17:28:19 1998 +0200 (1998-08-13)
changeset 53083ca4da83012c
parent 5307 6a699d5cdef4
child 5309 01c2b317da88
stac
NEWS
     1.1 --- a/NEWS	Wed Aug 12 17:40:18 1998 +0200
     1.2 +++ b/NEWS	Thu Aug 13 17:28:19 1998 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  
     1.5  * calling (stac rew i) now fails if "rew" has no effect on the goal
     1.6    [previously, this check worked only if the rewrite rule was unconditional]
     1.7 -
     1.8 +  Now rew can involve either definitions or equalities (either == or =).
     1.9  
    1.10  *** ZF ***
    1.11  
    1.12 @@ -242,6 +242,7 @@
    1.13  
    1.14  * calling (stac rew i) now fails if "rew" has no effect on the goal
    1.15    [previously, this check worked only if the rewrite rule was unconditional]
    1.16 +  Now rew can involve either definitions or equalities (either == or =).
    1.17  
    1.18  * case_tac provided for compatibility with HOL
    1.19      (like the old excluded_middle_tac, but with subgoals swapped)