src/HOL/Nat.thy
changeset 35416 d8d7d1b785af
parent 35216 7641e8d831d2
child 35633 5da59c1ddece
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -45,8 +45,7 @@
     1.4    nat = Nat
     1.5    by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
     1.6  
     1.7 -constdefs
     1.8 -  Suc ::   "nat => nat"
     1.9 +definition Suc :: "nat => nat" where
    1.10    Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    1.11  
    1.12  local