equal
deleted
inserted
replaced
70 fun case_tac ctxt a fixes = |
70 fun case_tac ctxt a fixes = |
71 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}; |
71 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}; |
72 \<close> |
72 \<close> |
73 |
73 |
74 method_setup case_tac = \<open> |
74 method_setup case_tac = \<open> |
75 Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >> |
75 Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >> |
76 (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) |
76 (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) |
77 \<close> "case_tac emulation (dynamic instantiation!)" |
77 \<close> "case_tac emulation (dynamic instantiation!)" |
78 |
78 |
79 |
79 |
80 subsection \<open>Special elimination rules\<close> |
80 subsection \<open>Special elimination rules\<close> |