--- a/src/HOL/HOL.ML Tue Jan 28 16:21:15 1997 +0100
+++ b/src/HOL/HOL.ML Wed Jan 29 15:32:18 1997 +0100
@@ -313,7 +313,8 @@
fun stac th = CHANGED o rtac (th RS ssubst);
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
-(** strip proved goal while preserving !-bound var names **)
+
+(** strip ! and --> from proved goal while preserving !-bound var names **)
local
@@ -337,21 +338,12 @@
_ $ (Const("op -->",_)$_$_) => th RS mp
| _ => raise THM("RSmp",0,[th]));
+(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
fun normalize_thm funs =
let fun trans [] th = th
| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
in trans funs end;
-fun qed_spec_mp name =
- let val thm = normalize_thm [RSspec,RSmp] (result())
- in bind_thm(name, thm) end;
-
-fun qed_goal_spec_mp name thy s p =
- bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p =
- bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
-
end;