1.1 --- a/src/HOL/IntDiv.thy	Thu Apr 16 10:11:45 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Apr 16 14:02:11 2009 +0200
     1.3 @@ -249,33 +249,33 @@
     1.4  text {* Tool setup *}
     1.5  
     1.6  ML {*
     1.7 -local 
     1.8 +local
     1.9  
    1.10 -structure CancelDivMod = CancelDivModFun(
    1.11 -struct
    1.12 -  val div_name = @{const_name Divides.div};
    1.13 -  val mod_name = @{const_name Divides.mod};
    1.14 +structure CancelDivMod = CancelDivModFun(struct
    1.15 +
    1.16 +  val div_name = @{const_name div};
    1.17 +  val mod_name = @{const_name mod};
    1.18    val mk_binop = HOLogic.mk_binop;
    1.19    val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
    1.20    val dest_sum = Int_Numeral_Simprocs.dest_sum;
    1.21 -  val div_mod_eqs =
    1.22 -    map mk_meta_eq [@{thm zdiv_zmod_equality},
    1.23 -      @{thm zdiv_zmod_equality2}];
    1.24 +
    1.25 +  val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
    1.26 +
    1.27    val trans = trans;
    1.28 -  val prove_eq_sums =
    1.29 -    let
    1.30 -      val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
    1.31 -    in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
    1.32 +
    1.33 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
    1.34 +    (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
    1.35 +
    1.36  end)
    1.37  
    1.38  in
    1.39  
    1.40 -val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
    1.41 -  "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
    1.42 +val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
    1.43 +  "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    1.44  
    1.45 -end;
    1.46 +val _ = Addsimprocs [cancel_div_mod_int_proc];
    1.47  
    1.48 -Addsimprocs [cancel_zdiv_zmod_proc]
    1.49 +end
    1.50  *}
    1.51  
    1.52  lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"