--- a/src/HOL/Hoare/Arith2.thy Thu Dec 04 09:05:39 1997 +0100
+++ b/src/HOL/Hoare/Arith2.thy Thu Dec 04 09:05:59 1997 +0100
@@ -6,7 +6,7 @@
More arithmetic. Much of this duplicates ex/Primes.
*)
-Arith2 = Divides +
+Arith2 = Power +
constdefs
cd :: [nat, nat, nat] => bool
@@ -15,10 +15,9 @@
gcd :: [nat, nat] => nat
"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 (Suc 0) (%u v. m*v) n"
-
- fac :: nat => nat
- "fac m == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
+consts fac :: nat => nat
+primrec fac nat
+"fac 0 = Suc 0"
+"fac(Suc n) = (Suc n)*fac(n)"
end