--- a/src/HOL/Hoare/Arith2.ML Tue Sep 06 16:59:52 2005 +0200
+++ b/src/HOL/Hoare/Arith2.ML Tue Sep 06 16:59:53 2005 +0200
@@ -6,12 +6,8 @@
More arithmetic lemmas.
*)
-open Arith2;
-
-
(*** cd ***)
-
Goalw [cd_def] "0<n ==> cd n n n";
by (Asm_simp_tac 1);
qed "cd_nnn";
@@ -42,7 +38,7 @@
by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
qed "gcd_nnn";
-val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
+val prems = goalw (the_context ()) [gcd_def] "gcd m n = gcd n m";
by (simp_tac (simpset() addsimps [cd_swap]) 1);
qed "gcd_swap";
--- 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