src/FOL/IFOL_lemmas.ML

 
 val major::prems = Goal "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
 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;