--- a/src/HOL/Hoare/Arith2.thy Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Arith2.thy Fri Mar 08 13:11:09 1996 +0100
@@ -8,20 +8,20 @@
Arith2 = Arith +
-consts
- divides :: [nat, nat] => bool (infixl 70)
+constdefs
+ divides :: [nat, nat] => bool (infixl 70)
+ "x divides n == 0<n & 0<x & (n mod x) = 0"
+
cd :: [nat, nat, nat] => bool
- gcd :: [nat, nat] => nat
-
- pow :: [nat, nat] => nat (infixl 75)
- fac :: nat => nat
+ "cd x m n == x divides m & x divides n"
-defs
- divides_def "x divides n == 0<n & 0<x & (n mod x) = 0"
- cd_def "cd x m n == x divides m & x divides n"
- gcd_def "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+ gcd :: [nat, nat] => nat
+ "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
- pow_def "m pow n == nat_rec n (Suc 0) (%u v.m*v)"
- fac_def "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+ pow :: [nat, nat] => nat (infixl 75)
+ "m pow n == nat_rec n (Suc 0) (%u v.m*v)"
+
+ fac :: nat => nat
+ "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
end