--- a/src/HOL/Tools/Qelim/presburger.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed Mar 04 10:45:52 2009 +0100
@@ -122,14 +122,13 @@
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
- [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
+ [@{thm "dvd_eq_mod_eq_0"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
- @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
- @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
+ @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
- @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"},
+ @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_plus1"}]
@ @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
@@ -170,14 +169,14 @@
THEN_ALL_NEW simp_tac ss
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
THEN_ALL_NEW ObjectLogic.full_atomize_tac
- THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
+ THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
THEN_ALL_NEW ObjectLogic.full_atomize_tac
THEN_ALL_NEW div_mod_tac ctxt
THEN_ALL_NEW splits_tac ctxt
THEN_ALL_NEW simp_tac ss
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW nat_to_int_tac ctxt
- THEN_ALL_NEW core_cooper_tac ctxt
+ THEN_ALL_NEW (core_cooper_tac ctxt)
THEN_ALL_NEW finish_tac elim
end;