src/HOLCF/domain/theorems.ML

       val vns = map vname args;
       val eqn = %:x_name === con_app2 con %: vns;
       val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
     in Library.foldr mk_ex (vns, conj) end;
 
+  val conj_assoc = thm "conj_assoc";
   val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
   val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
   val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
   val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2;
 

 in
   val pat_rews = pat_stricts @ pat_apps;
 end;
 
 local
+  val rev_contrapos = thm "rev_contrapos";
   fun con_strict (con, args) = 
     let
       fun one_strict vn =
         let
           fun f arg = if vname arg = vn then UU else %# arg;

                  (filter_out is_lazy (snd (hd cons)))
     else [];
 end;
 
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
+val rev_contrapos = thm "rev_contrapos";
 
 val distincts_le =
   let
     fun dist (con1, args1) (con2, args2) =
       let