1.1 --- a/src/HOL/Divides.thy	Wed Feb 07 17:26:04 2007 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 07 17:26:49 2007 +0100
     1.3 @@ -32,9 +32,9 @@
     1.4    mod (infixl "mod" 70)
     1.5  
     1.6  instance nat :: "Divides.div"
     1.7 -  mod_def: "m mod n == wfrec (trancl pred_nat)
     1.8 +  mod_def: "m mod n == wfrec (pred_nat^+)
     1.9                            (%f j. if j<n | n=0 then j else f (j-n)) m"
    1.10 -  div_def:   "m div n == wfrec (trancl pred_nat) 
    1.11 +  div_def:   "m div n == wfrec (pred_nat^+) 
    1.12                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.13  
    1.14  definition
    1.15 @@ -61,10 +61,10 @@
    1.16                    standard]
    1.17  
    1.18  lemma mod_eq: "(%m. m mod n) = 
    1.19 -              wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
    1.20 +              wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
    1.21  by (simp add: mod_def)
    1.22  
    1.23 -lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)  
    1.24 +lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)  
    1.25                 (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
    1.26  by (simp add: div_def)
    1.27