equal
deleted
inserted
replaced
515 |
515 |
516 4. test for refl |
516 4. test for refl |
517 *) |
517 *) |
518 fun clean_tac lthy = |
518 fun clean_tac lthy = |
519 let |
519 let |
520 val defs = map (symmetric o #def) (qconsts_dest lthy) |
520 val defs = map (Thm.symmetric o #def) (qconsts_dest lthy) |
521 val prs = prs_rules_get lthy |
521 val prs = prs_rules_get lthy |
522 val ids = id_simps_get lthy |
522 val ids = id_simps_get lthy |
523 val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
523 val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
524 |
524 |
525 val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
525 val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |