# HG changeset patch
# User wenzelm
# Date 1126018793 -7200
# Node ID f27456a2a975658868fe8bc822a29a5abab98297
# Parent  ab45d65bf2044b0e60a5fd8a90e032c22cc20544
converted to Isar theory format;

diff -r ab45d65bf204 -r f27456a2a975 src/HOL/Hoare/Arith2.ML
--- 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";
 
diff -r ab45d65bf204 -r f27456a2a975 src/HOL/Hoare/Arith2.thy
--- 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