equal
deleted
inserted
replaced
254 | _ => Conv.all_conv ctrm |
254 | _ => Conv.all_conv ctrm |
255 end |
255 end |
256 |
256 |
257 val add_conv = More_Conv.bottom_conv add_simple_conv |
257 val add_conv = More_Conv.bottom_conv add_simple_conv |
258 |
258 |
259 fun add_tac ctxt = CONVERSION |
259 fun add_tac ctxt = CONVERSION (add_conv ctxt)*} |
260 (Conv.params_conv ~1 (fn ctxt => |
|
261 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
|
262 Conv.concl_conv ~1 (add_conv ctxt))) ctxt)*} |
|
263 |
260 |
264 text {* |
261 text {* |
265 A test case for this conversion is as follows |
262 A test case for this conversion is as follows |
266 *} |
263 *} |
267 |
264 |