src/HOL/Product_Type.thy
changeset 57016 c44ce6f4067d
parent 56626 6532efd66a70
child 57091 1fa9c19ba2c9
     1.1 --- a/src/HOL/Product_Type.thy	Tue May 20 15:59:16 2014 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue May 20 16:00:00 2014 +0200
     1.3 @@ -130,6 +130,22 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation unit :: linorder
     1.8 +begin
     1.9 +
    1.10 +definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
    1.11 +"less_eq_unit _ _ = True"
    1.12 +
    1.13 +definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
    1.14 +"less_unit _ _ = False"
    1.15 +
    1.16 +declare less_eq_unit_def [simp] less_unit_def [simp]
    1.17 +
    1.18 +instance
    1.19 +proof qed auto
    1.20 +
    1.21 +end
    1.22 +
    1.23  lemma [code]:
    1.24    "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
    1.25