stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
authorpaulson
Tue Jul 14 13:29:39 1998 +0200 (1998-07-14)
changeset 5139013ea0f023e3
parent 5138 b02dfb930bd9
child 5140 216a5dab14b6
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
even for conditional rewrites
src/FOL/IFOL.ML
src/HOL/HOL.ML
     1.1 --- a/src/FOL/IFOL.ML	Mon Jul 13 17:46:20 1998 +0200
     1.2 +++ b/src/FOL/IFOL.ML	Tue Jul 14 13:29:39 1998 +0200
     1.3 @@ -238,7 +238,9 @@
     1.4  
     1.5  (*Substitution: rule and tactic*)
     1.6  bind_thm ("ssubst", sym RS subst);
     1.7 -fun stac th = CHANGED o rtac (th RS ssubst);
     1.8 +
     1.9 +(*Fails unless the substitution has an effect*)
    1.10 +fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
    1.11  
    1.12  (*A special case of ex1E that would otherwise need quantifier expansion*)
    1.13  qed_goal "ex1_equalsE" IFOL.thy
     2.1 --- a/src/HOL/HOL.ML	Mon Jul 13 17:46:20 1998 +0200
     2.2 +++ b/src/HOL/HOL.ML	Tue Jul 14 13:29:39 1998 +0200
     2.3 @@ -343,7 +343,9 @@
     2.4  
     2.5  (** Standard abbreviations **)
     2.6  
     2.7 -fun stac th = CHANGED o rtac (th RS ssubst);
     2.8 +(*Fails unless the substitution has an effect*)
     2.9 +fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
    2.10 +
    2.11  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
    2.12  
    2.13