src/HOL/Codatatype/Tools/bnf_def_tactics.ML

   val mk_comp': thm -> thm
   val mk_in_mono_tac: int -> tactic
   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_set_natural': thm -> thm
 
-  val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+  val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+  val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_in_rel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
-  val mk_rel_converse_tac: thm -> tactic
-  val mk_rel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
+  val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
+  val mk_srel_converse_tac: thm -> tactic
+  val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
 end;
 
 structure BNF_Def_Tactics : BNF_DEF_TACTICS =
 struct
 

       rtac (map_comp RS trans RS sym), rtac map_cong,
       REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
         rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
         rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
 
-fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_id' map_comp set_naturals
+fun mk_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
   in
     if null set_naturals then
-      unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
-    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+      unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac subsetI,
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,

                 rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
             set_naturals])
           @{thms fst_convol snd_convol} [map_id', refl])] 1
   end;
 
-fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
   subst_tac ctxt [map_id] 1 THEN
     (if n = 0 then rtac refl 1
     else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
       rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
       CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
 
-fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt rel_O_Grs THEN
+fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt srel_O_Grs THEN
     EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
 
-fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals
+fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
   in
     if null set_naturals then
-      unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
-    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+      unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
       EVERY' [rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
         rtac @{thm relcompI}, rtac @{thm converseI},

           rtac (map_comp RS sym), rtac CollectI,
           CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
             etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   end;
 
-fun mk_rel_converse_tac le_converse =
+fun mk_srel_converse_tac le_converse =
   EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
     rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
 
-fun mk_rel_O_tac rel_O_Grs rel_Id map_cong map_wppull map_comp set_naturals
+fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
     fun in_tac nthO_in = rtac CollectI THEN'
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
           rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
   in
-    if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
-    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+    if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},

           rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
           rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
           rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
   end;
 
-fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} =
+fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} =
   let
     val ls' = replicate (Int.max (1, m)) ();
   in
-    unfold_thms_tac ctxt (rel_O_Grs @
+    unfold_thms_tac ctxt (srel_O_Grs @
       @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
     EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
       rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
       REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
       REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},