# HG changeset patch
# User haftmann
# Date 1179072923 -7200
# Node ID 8752ca7f849a8d2f6dd828d6bce96e3bac6c6a43
# Parent  f53486e661a762123a95f51100973b4cdd739839
tuned setup

diff -r f53486e661a7 -r 8752ca7f849a src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Sun May 13 18:15:22 2007 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Sun May 13 18:15:23 2007 +0200
@@ -9,7 +9,6 @@
 
 theory IntDiv
 imports IntArith "../Divides" "../FunDef"
-uses ("IntDiv_setup.ML")
 begin
 
 declare zless_nat_conj [simp]
@@ -245,7 +244,37 @@
 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
 by(simp add: mult_commute zmod_zdiv_equality[symmetric])
 
-use "IntDiv_setup.ML"
+text {* Tool setup *}
+
+ML_setup {*
+local 
+
+structure CancelDivMod = CancelDivModFun(
+struct
+  val div_name = @{const_name "Divides.div"};
+  val mod_name = @{const_name "Divides.mod"};
+  val mk_binop = HOLogic.mk_binop;
+  val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
+  val dest_sum = Int_Numeral_Simprocs.dest_sum;
+  val div_mod_eqs =
+    map mk_meta_eq [@{thm zdiv_zmod_equality},
+      @{thm zdiv_zmod_equality2}];
+  val trans = trans;
+  val prove_eq_sums =
+    let
+      val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
+    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
+end)
+
+in
+
+val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
+  ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc)
+
+end;
+
+Addsimprocs [cancel_zdiv_zmod_proc]
+*}
 
 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
 apply (cut_tac a = a and b = b in divAlg_correct)
diff -r f53486e661a7 -r 8752ca7f849a src/HOL/Integ/IntDiv_setup.ML
--- a/src/HOL/Integ/IntDiv_setup.ML	Sun May 13 18:15:22 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/Integ/IntDiv_setup.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow, Informatik, TU Muenchen
-    Copyright   2002  TU Muenchen
-
-Simproc for cancelling div and mod
-*)
-
-
-structure CancelDivModData =
-struct
-
-val div_name = "Divides.div";
-val mod_name = "Divides.mod";
-val mk_binop = HOLogic.mk_binop;
-val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
-val dest_sum = Int_Numeral_Simprocs.dest_sum;
-
-(*logic*)
-
-val div_mod_eqs =
-  map mk_meta_eq [thm"zdiv_zmod_equality",thm"zdiv_zmod_equality2"]
-
-val trans = trans
-
-val prove_eq_sums =
-  let val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
-  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
-
-end;
-
-structure CancelDivMod = CancelDivModFun(CancelDivModData);
-
-val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
-      ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc);
-
-Addsimprocs[cancel_zdiv_zmod_proc];