src/HOL/ex/coopertac.ML
changeset 23364 1f3b832c90c1
parent 23318 6d68b07ab5cf
child 23469 3f309f885d0b
     1.1 --- a/src/HOL/ex/coopertac.ML	Wed Jun 13 00:02:06 2007 +0200
     1.2 +++ b/src/HOL/ex/coopertac.ML	Wed Jun 13 03:28:21 2007 +0200
     1.3 @@ -92,15 +92,15 @@
     1.4      (* Simp rules for changing (n::int) to int n *)
     1.5      val simpset1 = HOL_basic_ss
     1.6        addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
     1.7 -        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
     1.8 +        [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
     1.9        addsplits [zdiff_int_split]
    1.10      (*simp rules for elimination of int n*)
    1.11  
    1.12      val simpset2 = HOL_basic_ss
    1.13 -      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
    1.14 -      addcongs [conj_le_cong, imp_le_cong]
    1.15 +      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
    1.16 +      addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}]
    1.17      (* simp rules for elimination of abs *)
    1.18 -    val simpset3 = HOL_basic_ss addsplits [abs_split]
    1.19 +    val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
    1.20      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    1.21      (* Theorem for the nat --> int transformation *)
    1.22      val pre_thm = Seq.hd (EVERY