src/HOL/Arith.thy
changeset 2099 c5f004bfcbab
parent 1824 44254696843a
child 2681 93ed51a91622
     1.1 --- a/src/HOL/Arith.thy	Tue Oct 15 16:40:04 1996 +0200
     1.2 +++ b/src/HOL/Arith.thy	Wed Oct 16 10:37:17 1996 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    div, mod  :: [nat, nat] => nat  (infixl 70)
     1.5  
     1.6  defs
     1.7 -  pred_def  "pred(m) == nat_rec 0 (%n r.n) m"
     1.8 +  pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
     1.9    add_def   "m+n == nat_rec n (%u v. Suc(v)) m"
    1.10    diff_def  "m-n == nat_rec m (%u v. pred(v)) n"
    1.11    mult_def  "m*n == nat_rec 0 (%u v. n + v) m"