equal
deleted
inserted
replaced
147 |
147 |
148 lemmas [quotient_thm] = |
148 lemmas [quotient_thm] = |
149 fun_quotient list_quotient |
149 fun_quotient list_quotient |
150 |
150 |
151 lemmas [quotient_rsp] = |
151 lemmas [quotient_rsp] = |
152 quot_rel_rsp nil_rsp cons_rsp |
152 quot_rel_rsp nil_rsp cons_rsp foldl_rsp |
153 |
153 |
154 ML {* maps_lookup @{theory} "List.list" *} |
154 ML {* maps_lookup @{theory} "List.list" *} |
155 ML {* maps_lookup @{theory} "*" *} |
155 ML {* maps_lookup @{theory} "*" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
157 |
157 |
1102 |
1102 |
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 #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} |
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 |
1111 @ defs |
1112 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1112 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |