src/HOL/Hoare/Arith2.thy
changeset 1824 44254696843a
parent 1558 9c6ebfab4e05
child 3372 6e472c8f0011
     1.1 --- a/src/HOL/Hoare/Arith2.thy	Fri Jun 21 13:51:09 1996 +0200
     1.2 +++ b/src/HOL/Hoare/Arith2.thy	Tue Jun 25 13:11:29 1996 +0200
     1.3 @@ -19,9 +19,9 @@
     1.4    "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
     1.5  
     1.6    pow     :: [nat, nat] => nat                              (infixl 75)
     1.7 -  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
     1.8 +  "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
     1.9  
    1.10    fac     :: nat => nat
    1.11 -  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    1.12 +  "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
    1.13  
    1.14  end