src/HOL/Decision_Procs/mir_tac.ML
 changeset 30939 207ec81543f6 parent 30509 e19d5b459a61 child 31240 2c20bcd70fbe
equal inserted replaced
30938:c6c9359e474c 30939:207ec81543f6
`    97                                   @{thm "mod_self"}, @{thm "zmod_self"},`
`    97                                   @{thm "mod_self"}, @{thm "zmod_self"},`
`    98                                   @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},`
`    98                                   @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},`
`    99                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},`
`    99                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},`
`   100                                   @{thm "Suc_plus1"}]`
`   100                                   @{thm "Suc_plus1"}]`
`   101                         addsimps @{thms add_ac}`
`   101                         addsimps @{thms add_ac}`
`   102                         addsimprocs [cancel_div_mod_proc]`
`   102                         addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]`
`   103     val simpset0 = HOL_basic_ss`
`   103     val simpset0 = HOL_basic_ss`
`   104       addsimps [mod_div_equality', Suc_plus1]`
`   104       addsimps [mod_div_equality', Suc_plus1]`
`   105       addsimps comp_ths`
`   105       addsimps comp_ths`
`   106       addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]`
`   106       addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]`
`   107     (* Simp rules for changing (n::int) to int n *)`
`   107     (* Simp rules for changing (n::int) to int n *)`