equal
deleted
inserted
replaced
136 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
136 Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' |
137 Splitter.split_tac (split_if :: splits) ORELSE' |
137 Splitter.split_tac (split_if :: splits) ORELSE' |
138 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
138 eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' |
139 etac notE THEN' atac ORELSE' |
139 etac notE THEN' atac ORELSE' |
140 (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def |
140 (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def |
141 sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE' |
141 sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @ |
|
142 mapsx @ map_comps @ map_idents))) ORELSE' |
142 fo_rtac @{thm cong} ctxt ORELSE' |
143 fo_rtac @{thm cong} ctxt ORELSE' |
143 rtac @{thm ext})); |
144 rtac @{thm ext})); |
144 |
145 |
145 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
146 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = |
146 HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |
147 HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' |