src/HOL/Tools/inductive_package.ML
changeset 6427 fd36b2e7d80e
parent 6424 ceab9e663e08
child 6430 69400c97d3bf
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Apr 14 14:44:04 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 14 15:58:01 1999 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  
     1.5  fun prove_mono setT fp_fun monos thy =
     1.6    let
     1.7 -    val _ = message "  Proving monotonicity...";
     1.8 +    val _ = message "  Proving monotonicity ...";
     1.9  
    1.10      val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
    1.11        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.12 @@ -252,7 +252,7 @@
    1.13  
    1.14  fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
    1.15    let
    1.16 -    val _ = message "  Proving the introduction rules...";
    1.17 +    val _ = message "  Proving the introduction rules ...";
    1.18  
    1.19      val unfold = standard (mono RS (fp_def RS
    1.20        (if coind then def_gfp_Tarski else def_lfp_Tarski)));
    1.21 @@ -284,7 +284,7 @@
    1.22  
    1.23  fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
    1.24    let
    1.25 -    val _ = message "  Proving the elimination rules...";
    1.26 +    val _ = message "  Proving the elimination rules ...";
    1.27  
    1.28      val rules1 = [CollectE, disjE, make_elim vimageD];
    1.29      val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
    1.30 @@ -335,7 +335,7 @@
    1.31  fun prove_indrule cs cTs sumT rec_const params intr_ts mono
    1.32      fp_def rec_sets_defs thy =
    1.33    let
    1.34 -    val _ = message "  Proving the induction rule...";
    1.35 +    val _ = message "  Proving the induction rule ...";
    1.36  
    1.37      val sign = Theory.sign_of thy;
    1.38