# HG changeset patch
# User nipkow
# Date 1400594400 -7200
# Node ID c44ce6f4067d98447d5e8c1a5b6c73929a88a2f4
# Parent  842bb6d362639944684aa21467d18d619552777a
added unit :: linorder

diff -r 842bb6d36263 -r c44ce6f4067d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue May 20 15:59:16 2014 +0200
+++ b/src/HOL/Product_Type.thy	Tue May 20 16:00:00 2014 +0200
@@ -130,6 +130,22 @@
 
 end
 
+instantiation unit :: linorder
+begin
+
+definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
+"less_eq_unit _ _ = True"
+
+definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
+"less_unit _ _ = False"
+
+declare less_eq_unit_def [simp] less_unit_def [simp]
+
+instance
+proof qed auto
+
+end
+
 lemma [code]:
   "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+