--- 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 *}