src/HOL/HOL.ML
changeset 2442 6663e0d210b0
parent 2031 03a843f0f447
child 2562 d571d6660240
     1.1 --- a/src/HOL/HOL.ML	Wed Dec 18 15:10:33 1996 +0100
     1.2 +++ b/src/HOL/HOL.ML	Wed Dec 18 15:11:07 1996 +0100
     1.3 @@ -123,6 +123,8 @@
     1.4  qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
     1.5   (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
     1.6  
     1.7 +bind_thm ("classical2", notE RS notI);
     1.8 +
     1.9  qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
    1.10   (fn _ => [REPEAT (ares_tac [notE] 1)]);
    1.11  
    1.12 @@ -344,6 +346,12 @@
    1.13    let val thm = normalize_thm [RSspec,RSmp] (result())
    1.14    in bind_thm(name, thm) end;
    1.15  
    1.16 +fun qed_goal_spec_mp name thy s p = 
    1.17 +	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
    1.18 +
    1.19 +fun qed_goalw_spec_mp name thy defs s p = 
    1.20 +	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
    1.21 +
    1.22  end;
    1.23  
    1.24