--- a/src/FOL/IFOL_lemmas.ML Thu Sep 07 20:47:54 2000 +0200
+++ b/src/FOL/IFOL_lemmas.ML Thu Sep 07 20:48:34 2000 +0200
@@ -424,64 +424,3 @@
by (rtac (major RS disjE) 1);
by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
qed "disj_imp_disj";
-
-
-(** strip ALL and --> from proved goal while preserving ALL-bound var names **)
-
-fun make_new_spec rl =
- (* Use a crazy name to avoid forall_intr failing because of
- duplicate variable name *)
- let val myspec = read_instantiate [("P","?wlzickd")] rl
- val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
- val cvx = cterm_of (#sign(rep_thm myspec)) vx
- in (vxT, forall_intr cvx myspec) end;
-
-local
-
-val (specT, spec') = make_new_spec spec
-
-in
-
-fun RSspec th =
- (case concl_of th of
- _ $ (Const("All",_) $ Abs(a,_,_)) =>
- let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT))
- in th RS forall_elim ca spec' end
- | _ => raise THM("RSspec",0,[th]));
-
-fun RSmp th =
- (case concl_of th of
- _ $ (Const("op -->",_)$_$_) => th RS mp
- | _ => raise THM("RSmp",0,[th]));
-
-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;
-
-
-(* attributes *)
-
-local
-
-fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
-
-in
-
-val attrib_setup =
- [Attrib.add_attributes
- [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
-
-end;