785 fun quotient_tac ctxt quot_thms =

   785 fun quotient_tac ctxt quot_thms =

   786   REPEAT_ALL_NEW (FIRST'

   786   REPEAT_ALL_NEW (FIRST'

   787     [rtac @{thm FUN_QUOTIENT},

   787     [rtac @{thm FUN_QUOTIENT},

   788      resolve_tac quot_thms,

   788      resolve_tac quot_thms,

   789      rtac @{thm IDENTITY_QUOTIENT},

   789      rtac @{thm IDENTITY_QUOTIENT},

   790      (* For functional identity quotients, (op = ---> op =) *)

   791      (* For functional identity quotients, (op = ---> op =) *)

   791      (* TODO: think about the other way around, if we need to shorten the relation *)

   792      (* TODO: think about the other way around, if we need to shorten the relation *)

   792      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])

   793      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])

   793 *}

   794 *}

   794 

   795 

  1220     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot

  1221     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot

  1221     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same

  1222     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same

  1222     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps

  1223     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps

  1223       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)

  1224       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)

  1224   in

  1225   in

  1226             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),

  1227             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),

  1227             TRY o simp_tac simp_ctxt,

  1228             TRY o simp_tac simp_ctxt,

  1228             TRY o rtac refl]

  1229             TRY o rtac refl]

  1229   end

  1230   end

  1230 *}

  1231 *}