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 @ (prs_rules_get lthy) |
1058 val thms1 = @{thms all_prs ex_prs} @ defs |
1059 val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) |
1059 val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1060 @ @{thms Quotient_abs_rep Quotient_rel_rep} |
|
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1060 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1062 in |
1061 in |
1063 EVERY' [lambda_prs_tac lthy, |
1062 EVERY' [lambda_prs_tac lthy, |
1064 simp_tac (simps thms1), |
1063 simp_tac (simps thms1), |
1065 simp_tac (simps thms2), |
1064 simp_tac (simps thms2), |