equal
deleted
inserted
replaced
156 val thy = ProofContext.theory_of ctxt |
156 val thy = ProofContext.theory_of ctxt |
157 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
157 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
158 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
158 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
159 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
159 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
160 val simpset = (mk_minimal_ss ctxt) |
160 val simpset = (mk_minimal_ss ctxt) |
161 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
161 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp id_simps} |
162 addsimprocs [simproc] |
162 addsimprocs [simproc] |
163 addSolver equiv_solver addSolver quotient_solver |
163 addSolver equiv_solver addSolver quotient_solver |
164 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
164 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
165 in |
165 in |
166 simp_tac simpset THEN' |
166 simp_tac simpset THEN' |