--- a/src/HOL/Hoare/Arith2.thy Fri May 30 15:20:41 1997 +0200
+++ b/src/HOL/Hoare/Arith2.thy Fri May 30 15:21:21 1997 +0200
@@ -3,17 +3,14 @@
Author: Norbert Galm
Copyright 1995 TUM
-More arithmetic.
+More arithmetic. Much of this duplicates ex/Primes.
*)
-Arith2 = Arith +
+Arith2 = Divides +
constdefs
- divides :: [nat, nat] => bool (infixl 70)
- "x divides n == 0<n & 0<x & (n mod x) = 0"
-
cd :: [nat, nat, nat] => bool
- "cd x m n == x divides m & x divides n"
+ "cd x m n == x dvd m & x dvd n"
gcd :: [nat, nat] => nat
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"