equal
deleted
inserted
replaced
839 LAMBDA_RES_TAC ctxt, |
839 LAMBDA_RES_TAC ctxt, |
840 ball_rsp_tac ctxt, |
840 ball_rsp_tac ctxt, |
841 bex_rsp_tac ctxt, |
841 bex_rsp_tac ctxt, |
842 FIRST' (map rtac rsp_thms), |
842 FIRST' (map rtac rsp_thms), |
843 rtac refl, |
843 rtac refl, |
844 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
844 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])), |
845 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
845 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), |
846 Cong_Tac.cong_tac @{thm cong}, |
846 Cong_Tac.cong_tac @{thm cong}, |
847 rtac @{thm ext}, |
847 rtac @{thm ext}, |
848 rtac reflex_thm, |
848 rtac reflex_thm, |
849 atac, |
849 atac, |
850 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
850 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |