# HG changeset patch # User wenzelm # Date 965422571 -7200 # Node ID de95b5125580b27d44067b405f3a3d2b0b2a890c # Parent e20323caff4793688e3e3a71a8e5d0b972dd8e18 removed stac (now exported by HypsubstFun); diff -r e20323caff47 -r de95b5125580 src/FOL/IFOL_lemmas.ML --- a/src/FOL/IFOL_lemmas.ML Fri Aug 04 22:55:08 2000 +0200 +++ b/src/FOL/IFOL_lemmas.ML Fri Aug 04 22:56:11 2000 +0200 @@ -290,17 +290,9 @@ by (rtac refl 1); qed "meta_eq_to_obj_eq"; - -(*Substitution: rule and tactic*) +(*substitution*) bind_thm ("ssubst", sym RS subst); -(*Apply an equality or definition ONCE. - Fails unless the substitution has an effect*) -fun stac th = - let val th' = th RS meta_eq_to_obj_eq handle THM _ => th - in CHANGED_GOAL (rtac (th' RS ssubst)) - end; - (*A special case of ex1E that would otherwise need quantifier expansion*) val prems = Goal "[| EX! x. P(x); P(a); P(b) |] ==> a=b"; diff -r e20323caff47 -r de95b5125580 src/HOL/HOL_lemmas.ML --- a/src/HOL/HOL_lemmas.ML Fri Aug 04 22:55:08 2000 +0200 +++ b/src/HOL/HOL_lemmas.ML Fri Aug 04 22:56:11 2000 +0200 @@ -488,13 +488,6 @@ (** Standard abbreviations **) -(*Apply an equality or definition ONCE. - Fails unless the substitution has an effect*) -fun stac th = - let val th' = th RS def_imp_eq handle THM _ => th - in CHANGED_GOAL (rtac (th' RS ssubst)) - end; - (* combination of (spec RS spec RS ...(j times) ... spec RS mp *) local fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t