src/HOL/HOL.ML
changeset 6968 7f2977e96a5c
parent 6513 e0a9459e99fc
child 7030 53934985426a
equal deleted inserted replaced
6967:a3c163ed1e04 6968:7f2977e96a5c
   370 (** Standard abbreviations **)
   370 (** Standard abbreviations **)
   371 
   371 
   372 (*Apply an equality or definition ONCE.
   372 (*Apply an equality or definition ONCE.
   373   Fails unless the substitution has an effect*)
   373   Fails unless the substitution has an effect*)
   374 fun stac th = 
   374 fun stac th = 
   375   let val th' = th RS def_imp_eq handle _ => th
   375   let val th' = th RS def_imp_eq handle THM _ => th
   376   in  CHANGED_GOAL (rtac (th' RS ssubst))
   376   in  CHANGED_GOAL (rtac (th' RS ssubst))
   377   end;
   377   end;
   378 
   378 
   379 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   379 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   380 
   380