src/HOL/Tools/datatype_rep_proofs.ML
changeset 6427 fd36b2e7d80e
parent 6422 965705537d5b
child 6522 2f6cec5c046f
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Apr 14 14:44:04 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Apr 14 15:58:01 1999 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5      (************** generate introduction rules for representing set **********)
     1.6  
     1.7 -    val _ = message "Constructing representing sets...";
     1.8 +    val _ = message "Constructing representing sets ...";
     1.9  
    1.10      (* make introduction rule for a single constructor *)
    1.11  
    1.12 @@ -215,7 +215,7 @@
    1.13  
    1.14      (*********** isomorphisms for new types (introduced by typedef) ***********)
    1.15  
    1.16 -    val _ = message "Proving isomorphism properties...";
    1.17 +    val _ = message "Proving isomorphism properties ...";
    1.18  
    1.19      (* get axioms from theory *)
    1.20  
    1.21 @@ -439,7 +439,7 @@
    1.22  
    1.23      (******************* freeness theorems for constructors *******************)
    1.24  
    1.25 -    val _ = message "Proving freeness of constructors...";
    1.26 +    val _ = message "Proving freeness of constructors ...";
    1.27  
    1.28      (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
    1.29      
    1.30 @@ -491,7 +491,7 @@
    1.31  
    1.32      (*************************** induction theorem ****************************)
    1.33  
    1.34 -    val _ = message "Proving induction rule for datatypes...";
    1.35 +    val _ = message "Proving induction rule for datatypes ...";
    1.36  
    1.37      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
    1.38        (map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));