equal
deleted
inserted
replaced
474 done |
474 done |
475 |
475 |
476 method_setup eq_coinduct3 = {* |
476 method_setup eq_coinduct3 = {* |
477 Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => |
477 Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => |
478 SIMPLE_METHOD' |
478 SIMPLE_METHOD' |
479 (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) |
479 (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3})) |
480 *} |
480 *} |
481 |
481 |
482 |
482 |
483 subsection {* Untyped Case Analysis and Other Facts *} |
483 subsection {* Untyped Case Analysis and Other Facts *} |
484 |
484 |