src/HOL/Divides.thy

     (simp add: divmod_nat_div_mod)
 
 text {* Simproc for cancelling @{const div} and @{const mod} *}
 
 ML {*
-local
-
-structure CancelDivMod = CancelDivModFun
+structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
 (
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
   val mk_sum = Nat_Arith.mk_sum;

   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
 )
-
-in
-
-val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
-  "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
-
-val _ = Addsimprocs [cancel_div_mod_nat_proc];
-
-end
 *}
+
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
 
 
 subsubsection {* Quotient *}
 
 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"

 by(simp add: mult_commute zmod_zdiv_equality[symmetric])
 
 text {* Tool setup *}
 
 ML {*
-local
-
-structure CancelDivMod = CancelDivModFun
+structure Cancel_Div_Mod_Int = Cancel_Div_Mod
 (
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
   val mk_sum = Arith_Data.mk_sum HOLogic.intT;

   val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
 
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
     (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
 )
-
-in
-
-val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
-  "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
-
-val _ = Addsimprocs [cancel_div_mod_int_proc];
-
-end
 *}
+
+simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.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 divmod_int_correct)
 apply (auto simp add: divmod_int_rel_def mod_int_def)
 done