diff -r 0140cc7b26ad -r d0b74fdd6067 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Dec 05 14:15:39 2007 +0100
+++ b/src/HOL/Product_Type.thy	Wed Dec 05 14:15:45 2007 +0100
@@ -24,6 +24,17 @@
 declare case_split [cases type: bool]
   -- "prefer plain propositional version"
 
+lemma [code func]:
+  shows "False = P \<longleftrightarrow> \<not> P"
+    and "True = P \<longleftrightarrow> P" 
+    and "P = False \<longleftrightarrow> \<not> P" 
+    and "P = True \<longleftrightarrow> P" by simp_all
+
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_instance bool :: eq
+  (Haskell -)
 
 subsection {* Unit *}