Added theorems True_not_False and False_not_True
(for rep_datatype).

--- 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]);