--- a/src/HOL/Hoare/Arith2.thy Tue Sep 06 16:59:52 2005 +0200
+++ b/src/HOL/Hoare/Arith2.thy Tue Sep 06 16:59:53 2005 +0200
@@ -6,19 +6,23 @@
More arithmetic. Much of this duplicates ex/Primes.
*)
-Arith2 = Main +
+theory Arith2
+imports Main
+begin
constdefs
- cd :: [nat, nat, nat] => bool
+ "cd" :: "[nat, nat, nat] => bool"
"cd x m n == x dvd m & x dvd n"
- gcd :: [nat, nat] => nat
+ gcd :: "[nat, nat] => nat"
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
-consts fac :: nat => nat
+consts fac :: "nat => nat"
primrec
"fac 0 = Suc 0"
"fac(Suc n) = (Suc n)*fac(n)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end