src/HOL/Tools/BNF/bnf_def.ML

   val rel_OO_Grp_of_bnf: bnf -> thm
   val rel_cong_of_bnf: bnf -> thm
   val rel_conversep_of_bnf: bnf -> thm
   val rel_mono_of_bnf: bnf -> thm
   val rel_mono_strong0_of_bnf: bnf -> thm
+  val rel_mono_strong_of_bnf: bnf -> thm
   val rel_eq_of_bnf: bnf -> thm
   val rel_flip_of_bnf: bnf -> thm
   val set_bd_of_bnf: bnf -> thm list
   val set_defs_of_bnf: bnf -> thm list
   val set_map0_of_bnf: bnf -> thm list

   set_map: thm lazy list,
   rel_cong: thm lazy,
   rel_map: thm list lazy,
   rel_mono: thm lazy,
   rel_mono_strong0: thm lazy,
+  rel_mono_strong: thm lazy,
   rel_Grp: thm lazy,
   rel_conversep: thm lazy,
   rel_OO: thm lazy
 };
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
     inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
-    rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO = {
+    rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp rel_conversep rel_OO = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
   collect_set_map = collect_set_map,
   in_bd = in_bd,

   set_map = set_map,
   rel_cong = rel_cong,
   rel_map = rel_map,
   rel_mono = rel_mono,
   rel_mono_strong0 = rel_mono_strong0,
+  rel_mono_strong = rel_mono_strong,
   rel_Grp = rel_Grp,
   rel_conversep = rel_conversep,
   rel_OO = rel_OO};
 
 fun map_facts f {

   set_map,
   rel_cong,
   rel_map,
   rel_mono,
   rel_mono_strong0,
+  rel_mono_strong,
   rel_Grp,
   rel_conversep,
   rel_OO} =
   {bd_Card_order = f bd_Card_order,
     bd_Cinfinite = f bd_Cinfinite,

     set_map = map (Lazy.map f) set_map,
     rel_cong = Lazy.map f rel_cong,
     rel_map = Lazy.map (map f) rel_map,
     rel_mono = Lazy.map f rel_mono,
     rel_mono_strong0 = Lazy.map f rel_mono_strong0,
+    rel_mono_strong = Lazy.map f rel_mono_strong,
     rel_Grp = Lazy.map f rel_Grp,
     rel_conversep = Lazy.map f rel_conversep,
     rel_OO = Lazy.map f rel_OO};
 
 val morph_facts = map_facts o Morphism.thm;

 val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
 val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
 val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
+val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
 val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
 val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
 val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
 val wit_thms_of_bnf = maps #prop o wits_of_bnf;

 val rel_GrpN = "rel_Grp";
 val rel_conversepN = "rel_conversep";
 val rel_mapN = "rel_map"
 val rel_monoN = "rel_mono"
 val rel_mono_strong0N = "rel_mono_strong0"
+val rel_mono_strongN = "rel_mono_strong"
 val rel_comppN = "rel_compp";
 val rel_compp_GrpN = "rel_compp_Grp";
 
 datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
 

            (in_relN, [Lazy.force (#in_rel facts)]),
            (inj_mapN, [Lazy.force (#inj_map facts)]),
            (map_comp0N, [#map_comp0 axioms]),
            (map_transferN, [Lazy.force (#map_transfer facts)]),
            (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
+           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
            (set_map0N, #set_map0 axioms),
            (set_bdN, #set_bd axioms)] @
           (witNs ~~ wit_thmss_of_bnf bnf)
           |> map (fn (thmN, thms) =>
             ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),

             |> Thm.close_derivation
           end;
 
         val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
 
+        fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0)
+
+        val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
+
         fun mk_rel_map () =
           let
             fun mk_goal lhs rhs =
               fold_rev Logic.all ([x, y] @ S_CsBs @ S_AsCs @ is @ gs) (mk_Trueprop_eq (lhs, rhs));
 

 
         val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
           in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
-          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO;
+          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
+          rel_conversep rel_OO;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
         val bnf_rel =
           Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;