equal
deleted
inserted
replaced
521 |
521 |
522 4. test for refl |
522 4. test for refl |
523 *) |
523 *) |
524 fun clean_tac lthy = |
524 fun clean_tac lthy = |
525 let |
525 let |
526 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy) |
526 val defs = map (symmetric o #def) (qconsts_dest lthy) |
527 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
|
528 val prs = prs_rules_get lthy |
527 val prs = prs_rules_get lthy |
529 val ids = id_simps_get lthy |
528 val ids = id_simps_get lthy |
530 val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
529 val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
531 |
530 |
532 val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
531 val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |