src/HOL/HOL.ML
changeset 5309 01c2b317da88
parent 5299 d15a4155b96b
child 5346 bc9748ad8491
     1.1 --- a/src/HOL/HOL.ML	Thu Aug 13 17:28:19 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Thu Aug 13 17:28:52 1998 +0200
     1.3 @@ -23,6 +23,11 @@
     1.4   (fn prems =>
     1.5          [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
     1.6  
     1.7 +val prems = goal thy "(A == B) ==> A = B";
     1.8 +by (rewrite_goals_tac prems);
     1.9 +by (rtac refl 1);
    1.10 +qed "def_imp_eq";
    1.11 +
    1.12  (*Useful with eresolve_tac for proving equalties from known equalities.
    1.13          a = b
    1.14          |   |
    1.15 @@ -353,8 +358,12 @@
    1.16  
    1.17  (** Standard abbreviations **)
    1.18  
    1.19 -(*Fails unless the substitution has an effect*)
    1.20 -fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
    1.21 +(*Apply an equality or definition ONCE.
    1.22 +  Fails unless the substitution has an effect*)
    1.23 +fun stac th = 
    1.24 +  let val th' = th RS def_imp_eq handle _ => th
    1.25 +  in  CHANGED_GOAL (rtac (th' RS ssubst))
    1.26 +  end;
    1.27  
    1.28  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
    1.29