src/HOL/Library/Extended_Nat.thy
 changeset 56777 9c3f0ae99532 parent 54419 0c50894fc0d9 child 57512 cc97b347b301
```     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:48:59 2014 +0200
1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:50:03 2014 +0200
1.3 @@ -615,19 +615,18 @@
1.4  begin
1.5
1.6  definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
1.7 -  "inf_enat \<equiv> min"
1.8 +  "inf_enat = min"
1.9
1.10  definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
1.11 -  "sup_enat \<equiv> max"
1.12 +  "sup_enat = max"
1.13
1.14  definition Inf_enat :: "enat set \<Rightarrow> enat" where
1.15 -  "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
1.16 +  "Inf_enat A = (if A = {} then \<infinity> else (LEAST x. x \<in> A))"
1.17
1.18  definition Sup_enat :: "enat set \<Rightarrow> enat" where
1.19 -  "Sup_enat A \<equiv> if A = {} then 0
1.20 -    else if finite A then Max A
1.21 -                     else \<infinity>"
1.22 -instance proof
1.23 +  "Sup_enat A = (if A = {} then 0 else if finite A then Max A else \<infinity>)"
1.24 +instance
1.25 +proof
1.26    fix x :: "enat" and A :: "enat set"
1.27    { assume "x \<in> A" then show "Inf A \<le> x"
1.28        unfolding Inf_enat_def by (auto intro: Least_le) }
```