src/HOL/Hoare/Arith2.thy

--- a/src/HOL/Hoare/Arith2.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -19,9 +19,9 @@
   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
 
   pow     :: [nat, nat] => nat                              (infixl 75)
-  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
+  "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
 
   fac     :: nat => nat
-  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+  "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
 
 end