new stac
authorpaulson
Tue Jul 14 13:33:12 1998 +0200 (1998-07-14)
changeset 5142c56aa8b59dc0
parent 5141 495a4f9af897
child 5143 b94cd208f073
new stac
NEWS
     1.1 --- a/NEWS	Tue Jul 14 13:31:55 1998 +0200
     1.2 +++ b/NEWS	Tue Jul 14 13:33:12 1998 +0200
     1.3 @@ -149,11 +149,17 @@
     1.4  
     1.5  * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
     1.6  
     1.7 +* calling (stac rew i) now fails if "rew" has no effect on the goal
     1.8 +  [previously, this check worked only if the rewrite rule was unconditional]
     1.9 +
    1.10  
    1.11  *** ZF ***
    1.12  
    1.13  * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
    1.14  
    1.15 +* calling (stac rew i) now fails if "rew" has no effect on the goal
    1.16 +  [previously, this check worked only if the rewrite rule was unconditional]
    1.17 +
    1.18  
    1.19  *** Internal programming interfaces ***
    1.20  
    1.21 @@ -170,6 +176,8 @@
    1.22  * Pure: several new basic modules made available for general use, see
    1.23  also src/Pure/README;
    1.24  
    1.25 +* new tactical CHANGED_GOAL for checking that a tactic modifies a subgoal
    1.26 +
    1.27  
    1.28  
    1.29  New in Isabelle98 (January 1998)