equal
deleted
inserted
replaced
162 Union_image_insert Union_image_empty}; |
162 Union_image_insert Union_image_empty}; |
163 |
163 |
164 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms = |
164 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms = |
165 ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN |
165 ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN |
166 unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN |
166 unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN |
167 REPEAT_DETERM ( |
167 REPEAT_DETERM ((atac ORELSE' |
168 atac 1 ORELSE |
168 REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN' |
169 REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN |
169 etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN' |
170 (TRY o dresolve_tac Gwit_thms THEN' |
|
171 (etac FalseE ORELSE' |
170 (etac FalseE ORELSE' |
172 hyp_subst_tac ctxt THEN' |
171 hyp_subst_tac ctxt THEN' |
173 dresolve_tac Fwit_thms THEN' |
172 dresolve_tac Fwit_thms THEN' |
174 (etac FalseE ORELSE' atac))) 1); |
173 (etac FalseE ORELSE' atac))) 1); |
175 |
174 |