787     rtac trans_thm,

   787     rtac trans_thm,

   788     LAMBDA_RES_TAC ctxt,

   788     LAMBDA_RES_TAC ctxt,

   789     ball_rsp_tac ctxt,

   789     ball_rsp_tac ctxt,

   790     bex_rsp_tac ctxt,

   790     bex_rsp_tac ctxt,

   791     FIRST' (map rtac rsp_thms),

   791     FIRST' (map rtac rsp_thms),

   792     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),

   793     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),

   794     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),

   794     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),

   795     Cong_Tac.cong_tac @{thm cong},

   795     Cong_Tac.cong_tac @{thm cong},

   796     rtac @{thm ext},

   796     rtac @{thm ext},

   797     rtac reflex_thm,

   797     rtac reflex_thm,

   798     atac,

   798     atac,