# HG changeset patch
# User Andreas Lochbihler
# Date 1402417493 -7200
# Node ID 697e0fad93370ef1ad36e6fd28db663083a870ed
# Parent  aab87ffa60cc8a78e758b1c35f8ccb7e30082554
add type class instances for unit

diff -r aab87ffa60cc -r 697e0fad9337 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Jun 10 12:16:22 2014 +0200
+++ b/src/HOL/Product_Type.thy	Tue Jun 10 18:24:53 2014 +0200
@@ -139,13 +139,30 @@
 definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
 "less_unit _ _ = False"
 
-declare less_eq_unit_def [simp] less_unit_def [simp]
+declare less_eq_unit_def [simp, abs_def, code_unfold] less_unit_def [simp, abs_def, code_unfold]
 
 instance
 proof qed auto
 
 end
 
+instantiation unit :: complete_boolean_algebra begin
+
+definition "top = ()"
+definition "bot = ()"
+definition [code_unfold]: "sup _ _ = ()"
+definition [code_unfold]: "inf _ _ = ()"
+definition "Sup _ = ()"
+definition "Inf _ = ()"
+definition [simp, code_unfold]: "uminus = (\<lambda>_ :: unit. ())"
+
+instance by intro_classes auto
+
+end
+
+instance unit :: "{complete_linorder, wellorder}"
+  by intro_classes auto
+
 lemma [code]:
   "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+