equal
deleted
inserted
replaced
259 @{thm zdiv_zmod_equality2}]; |
259 @{thm zdiv_zmod_equality2}]; |
260 val trans = trans; |
260 val trans = trans; |
261 val prove_eq_sums = |
261 val prove_eq_sums = |
262 let |
262 let |
263 val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac} |
263 val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac} |
264 in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end; |
264 in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end; |
265 end) |
265 end) |
266 |
266 |
267 in |
267 in |
268 |
268 |
269 val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ()) |
269 val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ()) |