# HG changeset patch
# User berghofe
# Date 909174975 -7200
# Node ID 7e2cf2820684683eef4b906e70b7b44c9848e6e8
# Parent  bf5d9e5b8cdf2b619738899be9daa4cacee7e27c
Added theorems True_not_False and False_not_True
(for rep_datatype).

diff -r bf5d9e5b8cdf -r 7e2cf2820684 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Oct 23 22:34:18 1998 +0200
+++ b/src/HOL/HOL.ML	Fri Oct 23 22:36:15 1998 +0200
@@ -129,6 +129,12 @@
 qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
 
+qed_goal "False_not_True" HOL.thy "False ~= True"
+  (K [rtac notI 1, etac False_neq_True 1]);
+
+qed_goal "True_not_False" HOL.thy "True ~= False"
+  (K [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
+
 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);