equal
deleted
inserted
replaced
68 apply (erule r2) |
68 apply (erule r2) |
69 apply (erule r1) |
69 apply (erule r1) |
70 done |
70 done |
71 |
71 |
72 ML {* |
72 ML {* |
73 fun case_tac ctxt a = |
73 fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} |
74 RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} |
|
75 *} |
74 *} |
76 |
75 |
77 method_setup case_tac = |
76 method_setup case_tac = |
78 {* Method.goal_args_ctxt Args.name case_tac *} |
77 {* Method.goal_args_ctxt Args.name case_tac *} |
79 "case_tac emulation (dynamic instantiation!)" |
78 "case_tac emulation (dynamic instantiation!)" |