1.1 --- a/src/FOL/ex/Nat.thy	Tue May 03 11:28:51 1994 +0200
     1.2 +++ b/src/FOL/ex/Nat.thy	Tue May 03 15:00:00 1994 +0200
     1.3 @@ -11,12 +11,12 @@
     1.4  *)
     1.5  
     1.6  Nat = FOL +
     1.7 -types   nat 0
     1.8 -arities nat         :: term
     1.9 -consts  "0"         :: "nat"    ("0")
    1.10 -        Suc         :: "nat=>nat"
    1.11 -        rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    1.12 -        "+"         :: "[nat, nat] => nat"              (infixl 60)
    1.13 +types   nat
    1.14 +arities nat :: term
    1.15 +consts  "0" :: "nat"    ("0")
    1.16 +        Suc :: "nat=>nat"
    1.17 +        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    1.18 +        "+" :: "[nat, nat] => nat"              (infixl 60)
    1.19  rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
    1.20          Suc_inject  "Suc(m)=Suc(n) ==> m=n"
    1.21          Suc_neq_0   "Suc(m)=0      ==> R"