src/HOL/HOL.ML
changeset 2562 d571d6660240
parent 2442 6663e0d210b0
child 3003 c5293a17afa6
equal deleted inserted replaced
2561:8ef656dbf4fa 2562:d571d6660240
   311 (** Standard abbreviations **)
   311 (** Standard abbreviations **)
   312 
   312 
   313 fun stac th = CHANGED o rtac (th RS ssubst);
   313 fun stac th = CHANGED o rtac (th RS ssubst);
   314 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   314 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   315 
   315 
   316 (** strip proved goal while preserving !-bound var names **)
   316 
       
   317 (** strip ! and --> from proved goal while preserving !-bound var names **)
   317 
   318 
   318 local
   319 local
   319 
   320 
   320 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   321 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   321 val myspec = read_instantiate [("P","?XXX")] spec;
   322 val myspec = read_instantiate [("P","?XXX")] spec;
   335 fun RSmp th =
   336 fun RSmp th =
   336   (case concl_of th of
   337   (case concl_of th of
   337      _ $ (Const("op -->",_)$_$_) => th RS mp
   338      _ $ (Const("op -->",_)$_$_) => th RS mp
   338   | _ => raise THM("RSmp",0,[th]));
   339   | _ => raise THM("RSmp",0,[th]));
   339 
   340 
       
   341 (*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
   340 fun normalize_thm funs =
   342 fun normalize_thm funs =
   341 let fun trans [] th = th
   343 let fun trans [] th = th
   342       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   344       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   343 in trans funs end;
   345 in trans funs end;
   344 
       
   345 fun qed_spec_mp name =
       
   346   let val thm = normalize_thm [RSspec,RSmp] (result())
       
   347   in bind_thm(name, thm) end;
       
   348 
       
   349 fun qed_goal_spec_mp name thy s p = 
       
   350 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
       
   351 
       
   352 fun qed_goalw_spec_mp name thy defs s p = 
       
   353 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
       
   354 
   346 
   355 end;
   347 end;
   356 
   348 
   357 
   349 
   358 (*Thus, assignments to the references claset and simpset are recorded
   350 (*Thus, assignments to the references claset and simpset are recorded