equal
deleted
inserted
replaced
1053 fun clean_tac lthy = |
1053 fun clean_tac lthy = |
1054 let |
1054 let |
1055 val thy = ProofContext.theory_of lthy; |
1055 val thy = ProofContext.theory_of lthy; |
1056 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1056 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1057 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1057 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1058 val thms1 = @{thms all_prs ex_prs} @ defs |
1058 val thms1 = @{thms all_prs ex_prs} @ defs @ (prs_rules_get lthy) |
1059 val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) |
1059 val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) |
1060 @ @{thms Quotient_abs_rep Quotient_rel_rep} |
1060 @ @{thms Quotient_abs_rep Quotient_rel_rep} |
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1062 in |
1062 in |
1063 EVERY' [lambda_prs_tac lthy, |
1063 EVERY' [lambda_prs_tac lthy, |