--- 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";
--- 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