1.1 --- a/src/Sequents/LK/Nat.thy	Thu Feb 28 14:10:54 2013 +0100
     1.2 +++ b/src/Sequents/LK/Nat.thy	Thu Feb 28 14:22:14 2013 +0100
     1.3 @@ -11,20 +11,22 @@
     1.4  
     1.5  typedecl nat
     1.6  arities nat :: "term"
     1.7 -consts  Zero :: nat      ("0")
     1.8 -        Suc :: "nat=>nat"
     1.9 -        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    1.10 -        add :: "[nat, nat] => nat"                (infixl "+" 60)
    1.11  
    1.12 -axioms
    1.13 +axiomatization
    1.14 +  Zero :: nat      ("0") and
    1.15 +  Suc :: "nat=>nat" and
    1.16 +  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    1.17 +where
    1.18    induct:  "[| $H |- $E, P(0), $F;
    1.19 -              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
    1.20 +              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" and
    1.21  
    1.22 -  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
    1.23 -  Suc_neq_0:   "|- Suc(m) ~= 0"
    1.24 -  rec_0:       "|- rec(0,a,f) = a"
    1.25 +  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n" and
    1.26 +  Suc_neq_0:   "|- Suc(m) ~= 0" and
    1.27 +  rec_0:       "|- rec(0,a,f) = a" and
    1.28    rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    1.29 -  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
    1.30 +
    1.31 +definition add :: "[nat, nat] => nat"  (infixl "+" 60)
    1.32 +  where "m + n == rec(m, n, %x y. Suc(y))"
    1.33  
    1.34  
    1.35  declare Suc_neq_0 [simp]