| changeset 22483 | 86064f2f2188 |
| parent 22473 | 753123c89d72 |
| child 22718 | 936f7580937d |
--- a/src/HOL/Nat.thy Tue Mar 20 15:52:39 2007 +0100 +++ b/src/HOL/Nat.thy Tue Mar 20 15:52:40 2007 +0100 @@ -1324,6 +1324,11 @@ by (simp del: of_nat_add add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) +instance nat :: distrib_lattice + "inf \<equiv> min" + "sup \<equiv> max" + by intro_classes (auto simp add: inf_nat_def sup_nat_def) + subsection {* Size function *}