src/HOL/HOL.ML
changeset 2442 6663e0d210b0
parent 2031 03a843f0f447
child 2562 d571d6660240
equal deleted inserted replaced
2441:decc46a5cdb5 2442:6663e0d210b0
   121  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
   121  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
   122 
   122 
   123 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
   123 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
   124  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
   124  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
   125 
   125 
       
   126 bind_thm ("classical2", notE RS notI);
       
   127 
   126 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
   128 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
   127  (fn _ => [REPEAT (ares_tac [notE] 1)]);
   129  (fn _ => [REPEAT (ares_tac [notE] 1)]);
   128 
   130 
   129 
   131 
   130 (** Implication **)
   132 (** Implication **)
   342 
   344 
   343 fun qed_spec_mp name =
   345 fun qed_spec_mp name =
   344   let val thm = normalize_thm [RSspec,RSmp] (result())
   346   let val thm = normalize_thm [RSspec,RSmp] (result())
   345   in bind_thm(name, thm) end;
   347   in bind_thm(name, thm) end;
   346 
   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 
   347 end;
   355 end;
   348 
   356 
   349 
   357 
   350 (*Thus, assignments to the references claset and simpset are recorded
   358 (*Thus, assignments to the references claset and simpset are recorded
   351   with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
   359   with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)