equal
deleted
inserted
replaced
1089 |
1089 |
1090 ML {* |
1090 ML {* |
1091 fun clean_tac lthy quot = |
1091 fun clean_tac lthy quot = |
1092 let |
1092 let |
1093 val thy = ProofContext.theory_of lthy; |
1093 val thy = ProofContext.theory_of lthy; |
1094 val defs = map (#def) (qconsts_dest thy); |
1094 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1095 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1095 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1096 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1096 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1097 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1097 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1098 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1098 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1099 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1099 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |