--- a/src/HOL/Nat.thy Tue May 20 14:56:35 2014 +0200
+++ b/src/HOL/Nat.thy Tue May 20 16:28:05 2014 +0200
@@ -870,6 +870,10 @@
then show "P n" by auto
qed
+
+lemma Least_eq_0[simp]: "P(0::nat) \<Longrightarrow> Least P = 0"
+by (rule Least_equality[OF _ le0])
+
lemma Least_Suc:
"[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
apply (cases n, auto)
--- a/src/HOL/Product_Type.thy Tue May 20 14:56:35 2014 +0200
+++ b/src/HOL/Product_Type.thy Tue May 20 16:28:05 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+