equal
deleted
inserted
replaced
519 |
519 |
520 4. test for refl |
520 4. test for refl |
521 *) |
521 *) |
522 fun clean_tac lthy = |
522 fun clean_tac lthy = |
523 let |
523 let |
524 val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts lthy) |
524 val thy = Proof_Context.theory_of lthy |
|
525 val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy) |
525 val prs = Quotient_Info.prs_rules lthy |
526 val prs = Quotient_Info.prs_rules lthy |
526 val ids = Quotient_Info.id_simps lthy |
527 val ids = Quotient_Info.id_simps lthy |
527 val thms = |
528 val thms = |
528 @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
529 @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
529 |
530 |