equal
deleted
inserted
replaced
1103 ML {* |
1103 ML {* |
1104 fun clean_tac lthy = |
1104 fun clean_tac lthy = |
1105 let |
1105 let |
1106 val thy = ProofContext.theory_of lthy; |
1106 val thy = ProofContext.theory_of lthy; |
1107 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1107 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1108 val thms1 = @{thms all_prs ex_prs} |
1108 val thms1 = @{thms all_prs ex_prs} @ defs |
1109 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1109 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1110 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1110 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1111 @ defs |
|
1112 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1111 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1113 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1112 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1114 in |
1113 in |
1115 EVERY' [ |
1114 EVERY' [ |
1116 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |
1115 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |