src/HOL/Nat.thy
changeset 37387 3581483cca6c
parent 36977 71c8973a604b
child 37430 a77740fc3957
     1.1 --- a/src/HOL/Nat.thy	Tue Jun 08 07:45:39 2010 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jun 08 16:37:19 2010 +0200
     1.3 @@ -39,16 +39,11 @@
     1.4      Zero_RepI: "Nat Zero_Rep"
     1.5    | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
     1.6  
     1.7 -global
     1.8 -
     1.9 -typedef (open Nat)
    1.10 -  nat = Nat
    1.11 +typedef (open Nat) nat = Nat
    1.12    by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
    1.13  
    1.14  definition Suc :: "nat => nat" where
    1.15 -  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.16 -
    1.17 -local
    1.18 +  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    1.19  
    1.20  instantiation nat :: zero
    1.21  begin
    1.22 @@ -1457,8 +1452,7 @@
    1.23  end
    1.24  
    1.25  lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
    1.26 -unfolding mono_def
    1.27 -by (auto intro:lift_Suc_mono_le[of f])
    1.28 +  unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
    1.29  
    1.30  lemma mono_nat_linear_lb:
    1.31    "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"