QuotMain.thy
changeset 501 375e28eedee7
parent 499 f122816d7729
child 505 6cdba30c6d66
equal deleted inserted replaced
500:184d74813679 501:375e28eedee7
  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