src/HOL/Tools/Qelim/presburger.ML
changeset 31790 05c92381363c
parent 30936 d13cecf4ed4c
child 32603 e08fdd615333
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  val ss2 = HOL_basic_ss
     1.5    addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
     1.6              @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
     1.7 -            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
     1.8 +            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
     1.9    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    1.10  val div_mod_ss = HOL_basic_ss addsimps simp_thms 
    1.11    @ map (symmetric o mk_meta_eq) 
    1.12 @@ -129,7 +129,7 @@
    1.13       @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
    1.14       @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
    1.15       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
    1.16 -     @{thm "mod_1"}, @{thm "Suc_plus1"}]
    1.17 +     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
    1.18    @ @{thms add_ac}
    1.19   addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
    1.20   val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits