equal
deleted
inserted
replaced
175 |
175 |
176 fun arith_rew_tac ctxt prems = make_rew_tac ctxt |
176 fun arith_rew_tac ctxt prems = make_rew_tac ctxt |
177 (Arith_simp.norm_tac ctxt (congr_rls, prems)) |
177 (Arith_simp.norm_tac ctxt (congr_rls, prems)) |
178 |
178 |
179 fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt |
179 fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt |
180 (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems)) |
180 (Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, congr_rls, prems)) |
181 |
181 |
182 end |
182 end |
183 *} |
183 *} |
184 |
184 |
185 method_setup arith_rew = {* |
185 method_setup arith_rew = {* |