src/HOL/Product_Type.thy
changeset 20588 c847c56edf0c
parent 20415 e3d2d7b01279
child 21046 fe1db2f991a7
--- a/src/HOL/Product_Type.thy	Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Product_Type.thy	Tue Sep 19 15:21:42 2006 +0200
@@ -15,7 +15,7 @@
 
 typedef unit = "{True}"
 proof
-  show "True : ?unit" by blast
+  show "True : ?unit" ..
 qed
 
 constdefs
@@ -761,6 +761,29 @@
 
 subsection {* Code generator setup *}
 
+instance unit :: eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
+
+code_instance unit :: eq
+  (Haskell -)
+
+instance * :: (eq, eq) eq ..
+
+lemma [code func]:
+  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
+  unfolding eq_def by auto
+
+code_instance * :: eq
+  (Haskell -)
+
+code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
 types_code
   "*"     ("(_ */ _)")
 attach (term_of) {*