equal
deleted
inserted
replaced
1056 fun clean_tac lthy = |
1056 fun clean_tac lthy = |
1057 let |
1057 let |
1058 val thy = ProofContext.theory_of lthy; |
1058 val thy = ProofContext.theory_of lthy; |
1059 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1059 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1060 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1060 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1061 val thms1 = defs @ (prs_rules_get lthy) |
1061 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
1062 val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} |
1062 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1063 @ (id_simps_get lthy) |
|
1064 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1063 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1065 in |
1064 in |
1066 EVERY' [simp_tac (simps thms1), |
1065 EVERY' [simp_tac (simps thms1), |
|
1066 fun_map_tac lthy, |
|
1067 fun_map_tac lthy, |
|
1068 fun_map_tac lthy, |
1067 fun_map_tac lthy, |
1069 fun_map_tac lthy, |
1068 lambda_prs_tac lthy, |
1070 lambda_prs_tac lthy, |
1069 simp_tac (simps thms2), |
1071 simp_tac (simps thms2), |
1070 TRY o rtac refl] |
1072 TRY o rtac refl] |
1071 end |
1073 end |