src/HOL/Tools/datatype_abs_proofs.ML

 
 (************************ case distinction theorems ***************************)
 
 fun prove_casedist_thms new_type_names descr sorts induct thy =
   let
-    val _ = message "Proving case distinction theorems...";
+    val _ = message "Proving case distinction theorems ...";
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val newTs = take (length (hd descr), recTs);
 

 (*************************** primrec combinators ******************************)
 
 fun prove_primrec_thms flat_names new_type_names descr sorts
     (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
   let
-    val _ = message "Constructing primrec combinators...";
+    val _ = message "Constructing primrec combinators ...";
 
     val big_name = space_implode "_" new_type_names;
     val thy0 = add_path flat_names big_name thy;
 
     val descr' = flat descr;

         (InductivePackage.add_inductive_i false true big_rec_name' false false true
            rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
-    val _ = message "Proving termination and uniqueness of primrec functions...";
+    val _ = message "Proving termination and uniqueness of primrec functions ...";
 
     fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
       let
         val distinct_tac = (etac Pair_inject 1) THEN
           (if i < length newTs then

 
     val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
 
     (* prove characteristic equations for primrec combinators *)
 
-    val _ = message "Proving characteristic theorems for primrec combinators..."
+    val _ = message "Proving characteristic theorems for primrec combinators ..."
 
     val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
       (cterm_of (Theory.sign_of thy2) t) (fn _ =>
         [rtac select1_equality 1,
          resolve_tac rec_unique_thms 1,

 
 (***************************** case combinators *******************************)
 
 fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   let
-    val _ = message "Proving characteristic theorems for case combinators...";
+    val _ = message "Proving characteristic theorems for case combinators ...";
 
     val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;

 (******************************* case splitting *******************************)
 
 fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
     casedist_thms case_thms thy =
   let
-    val _ = message "Proving equations for case splitting...";
+    val _ = message "Proving equations for case splitting ...";
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val newTs = take (length (hd descr), recTs);
 

 
 (******************************* size functions *******************************)
 
 fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   let
-    val _ = message "Proving equations for size function...";
+    val _ = message "Proving equations for size function ...";
 
     val big_name = space_implode "_" new_type_names;
     val thy1 = add_path flat_names big_name thy;
 
     val descr' = flat descr;

 
 (************************* additional theorems for TFL ************************)
 
 fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
   let
-    val _ = message "Proving additional theorems for TFL...";
+    val _ = message "Proving additional theorems for TFL ...";
 
     fun prove_nchotomy (t, exhaustion) =
       let
         (* For goal i, select the correct disjunct to attack, then prove it *)
         fun tac i 0 = EVERY [TRY (rtac disjI1 i),