equal
deleted
inserted
replaced
156 (case find_eq ctxt (Thm.term_of ct) of |
156 (case find_eq ctxt (Thm.term_of ct) of |
157 NONE => NONE |
157 NONE => NONE |
158 | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); |
158 | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); |
159 |
159 |
160 val rearrange_eqs_simproc = |
160 val rearrange_eqs_simproc = |
161 Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"] |
161 Simplifier.make_simproc @{context} "rearrange_eqs" |
162 (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t)); |
162 {lhss = [@{term "Pure.all(t)"}], |
|
163 proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct, |
|
164 identifier = []}; |
163 |
165 |
164 |
166 |
165 (* rotate k premises to the left by j, skipping over first j premises *) |
167 (* rotate k premises to the left by j, skipping over first j premises *) |
166 |
168 |
167 fun rotate_conv 0 _ 0 = Conv.all_conv |
169 fun rotate_conv 0 _ 0 = Conv.all_conv |