--- a/src/HOL/Hoare/Arith2.thy Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/Hoare/Arith2.thy Wed Nov 29 17:01:41 1995 +0100
@@ -9,12 +9,12 @@
Arith2 = Arith +
consts
- divides :: "[nat, nat] => bool" (infixl 70)
- cd :: "[nat, nat, nat] => bool"
- gcd :: "[nat, nat] => nat"
+ divides :: [nat, nat] => bool (infixl 70)
+ cd :: [nat, nat, nat] => bool
+ gcd :: [nat, nat] => nat
- pow :: "[nat, nat] => nat" (infixl 75)
- fac :: "nat => nat"
+ pow :: [nat, nat] => nat (infixl 75)
+ fac :: nat => nat
defs
divides_def "x divides n == 0<n & 0<x & (n mod x) = 0"