src/HOL/BNF/Tools/bnf_gfp_tactics.ML

           EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
               then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
-                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
+                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, atac])
             (1 upto (m + n) ~~ set_naturals),
             rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
             REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])

         REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
         etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
         REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
         rtac trans, rtac map_cong,
-        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
+        REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         etac sym, rtac CollectI,
         CONJ_WRAP' (fn (i, thm) =>
           if i <= m
           then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
-            rtac @{thm diag_fst}, etac set_mp, atac]
+            rtac @{thm Id_on_fst}, etac set_mp, atac]
           else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
             rtac trans_fun_cong_image_id_id_apply, atac])
         (1 upto (m + n) ~~ set_naturals)];
   in
     EVERY' [rtac (bis_def RS trans),

     CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
       rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,
     CONJ_WRAP' (fn (srel_cong, srel_converse) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (srel_cong RS trans),
-        REPEAT_DETERM_N m o rtac @{thm diag_converse},
+        REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym),
         REPEAT_DETERM_N (length srel_congs) o rtac refl,
         rtac srel_converse,
         REPEAT_DETERM o etac allE,
         rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
 

     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
     CONJ_WRAP' (fn (srel_cong, srel_O) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (srel_cong RS trans),
-        REPEAT_DETERM_N m o rtac @{thm diag_Comp},
+        REPEAT_DETERM_N m o rtac @{thm Id_on_Comp},
         REPEAT_DETERM_N (length srel_congs) o rtac refl,
         rtac srel_O,
         etac @{thm relcompE},
         REPEAT_DETERM o dtac Pair_eqD,
         etac conjE, hyp_subst_tac,
         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
         etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
 
 fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
   {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
+  unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in,
         etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1},

 fun mk_incl_lsbis_tac n i lsbis_def =
   EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
     REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
     rtac (mk_nth_conv n i)] 1;
 
-fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
+fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
   EVERY' [rtac (@{thm equiv_def} RS iffD2),
 
     rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
     rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
-    rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
+    rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
 
     rtac conjI, rtac (@{thm sym_def} RS iffD2),
     rtac allI, rtac allI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
 

           rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis,
           rtac ord_eq_le_trans, rtac @{thm sym[OF relImage_relInvImage]},
           rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
           rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
           rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
-          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag},
+          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
           rtac Rep_inject])
       (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
   end;
 
 fun mk_unique_mor_tac raw_coinds bis =

       CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i),
         rtac @{thm subst[OF pair_in_Id_conv]}, etac set_mp,
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
+fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
     EVERY' (map (fn i =>
       EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
-        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
+        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on,
         rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
-        etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
+        etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
         rtac exI, rtac conjI, etac conjI, atac,
         CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
-          rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks])
+          rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks])
     ks),
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
 
 fun mk_map_tac m n cT unfold map_comp' map_cong =