equal
deleted
inserted
replaced
1079 fun clean_tac lthy = |
1079 fun clean_tac lthy = |
1080 let |
1080 let |
1081 val thy = ProofContext.theory_of lthy; |
1081 val thy = ProofContext.theory_of lthy; |
1082 val quotients = quotient_rules_get lthy |
1082 val quotients = quotient_rules_get lthy |
1083 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1083 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1084 val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients |
1084 val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients |
1085 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1085 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1086 val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients |
1086 val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients |
1087 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1087 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1088 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1088 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1089 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1089 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |