--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Nov 23 22:07:55 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Nov 23 22:59:39 2011 +0100
@@ -86,19 +86,21 @@
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_eq_plus1]
addsimps comp_arith
- addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
+ |> fold Splitter.add_split
+ [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
(* Simp rules for changing (n::int) to int n *)
val simpset1 = HOL_basic_ss
addsimps [@{thm nat_number_of_def}, zdvd_int] @ map (fn r => r RS sym)
[@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
- addsplits [zdiff_int_split]
+ |> Splitter.add_split zdiff_int_split
(*simp rules for elimination of int n*)
val simpset2 = HOL_basic_ss
- addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
- addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}]
+ addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat},
+ @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
+ |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
(* simp rules for elimination of abs *)
- val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
+ val simpset3 = HOL_basic_ss |> Splitter.add_split @{thm abs_split}
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY