Added theorems True_not_False and False_not_True
authorberghofe
Fri Oct 23 22:36:15 1998 +0200 (1998-10-23)
changeset 57607e2cf2820684
parent 5759 bf5d9e5b8cdf
child 5761 a396eff81fda
Added theorems True_not_False and False_not_True
(for rep_datatype).
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Fri Oct 23 22:34:18 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Oct 23 22:36:15 1998 +0200
     1.3 @@ -129,6 +129,12 @@
     1.4  qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
     1.5   (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
     1.6  
     1.7 +qed_goal "False_not_True" HOL.thy "False ~= True"
     1.8 +  (K [rtac notI 1, etac False_neq_True 1]);
     1.9 +
    1.10 +qed_goal "True_not_False" HOL.thy "True ~= False"
    1.11 +  (K [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
    1.12 +
    1.13  qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
    1.14   (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
    1.15