src/HOL/Decision_Procs/mir_tac.ML
changeset 61694 6571c78c9667
parent 61652 90c65a811257
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5    val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"},
     1.6                   @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)}] @
     1.7 -                 (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}])
     1.8 +                 (map (fn th => th RS sym) [@{thm "numeral_One"}])
     1.9                   @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} 
    1.10    val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
    1.11               @{thm of_nat_numeral},
    1.12 @@ -87,9 +87,8 @@
    1.13              @{thm "split_min"}, @{thm "split_max"}]
    1.14      (* Simp rules for changing (n::int) to int n *)
    1.15      val simpset1 = put_simpset HOL_basic_ss ctxt
    1.16 -      addsimps [@{thm "zdvd_int"}] @ map (fn r => r RS sym)
    1.17 -        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
    1.18 -         @{thm nat_numeral}, @{thm "zmult_int"}]
    1.19 +      addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ 
    1.20 +          map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm nat_numeral}]
    1.21        |> Splitter.add_split @{thm "zdiff_int_split"}
    1.22      (*simp rules for elimination of int n*)
    1.23