equal
deleted
inserted
replaced
524 val prs = prs_rules_get lthy |
524 val prs = prs_rules_get lthy |
525 val ids = id_simps_get lthy |
525 val ids = id_simps_get lthy |
526 |
526 |
527 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
527 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
528 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs ex1_prs}) |
528 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs ex1_prs}) |
529 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep ex1_prs} @ ids) |
529 val ss2 = mk_simps (@{thms Quotient_abs_rep[THEN eq_reflection] |
|
530 Quotient_rel_rep[THEN eq_reflection] ex1_prs} @ ids) |
530 in |
531 in |
531 EVERY' [simp_tac ss1, |
532 EVERY' [simp_tac ss1, |
532 fun_map_tac lthy, |
533 fun_map_tac lthy, |
533 lambda_prs_tac lthy, |
534 lambda_prs_tac lthy, |
534 simp_tac ss2, |
535 simp_tac ss2, |