equal
deleted
inserted
replaced
498 TRYALL Goal.conjunction_tac THEN |
498 TRYALL Goal.conjunction_tac THEN |
499 unfold_thms_tac ctxt ctr_defs' THEN |
499 unfold_thms_tac ctxt ctr_defs' THEN |
500 ALLGOALS (subst_tac ctxt NONE fp_sets) THEN |
500 ALLGOALS (subst_tac ctxt NONE fp_sets) THEN |
501 unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_nesting_set_maps @ |
501 unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_nesting_set_maps @ |
502 live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @ |
502 live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @ |
503 @{thms UN_UN_flatten UN_Un sup_assoc[THEN sym]}) THEN |
503 @{thms UN_UN_flatten UN_Un_distrib UN_Un sup_assoc[THEN sym]}) THEN |
504 ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN |
504 ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN |
505 ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN |
505 ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN |
506 ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt); |
506 ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt); |
507 |
507 |
508 fun mk_set_sel_tac ctxt ct exhaust discs sels sets = |
508 fun mk_set_sel_tac ctxt ct exhaust discs sels sets = |