Added quiet_mode flag.
authorberghofe
Fri Oct 16 18:55:34 1998 +0200 (1998-10-16)
changeset 566272a2e33d3b9e
parent 5661 6ecb6ea25f19
child 5663 aad79a127628
Added quiet_mode flag.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 16 18:54:55 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 16 18:55:34 1998 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4  
     1.5  signature INDUCTIVE_PACKAGE =
     1.6  sig
     1.7 +  val quiet_mode : bool ref
     1.8    val add_inductive_i : bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     1.9      term list -> thm list -> thm list -> theory -> theory *
    1.10        {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
    1.11 @@ -46,6 +47,9 @@
    1.12  structure InductivePackage : INDUCTIVE_PACKAGE =
    1.13  struct
    1.14  
    1.15 +val quiet_mode = ref false;
    1.16 +fun message s = if !quiet_mode then () else writeln s;
    1.17 +
    1.18  (*For proving monotonicity of recursion operator*)
    1.19  val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
    1.20                     ex_mono, Collect_mono, in_mono, vimage_mono];
    1.21 @@ -219,7 +223,7 @@
    1.22  
    1.23  fun prove_mono setT fp_fun monos thy =
    1.24    let
    1.25 -    val _ = writeln "  Proving monotonicity...";
    1.26 +    val _ = message "  Proving monotonicity...";
    1.27  
    1.28      val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop
    1.29        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.30 @@ -231,7 +235,7 @@
    1.31  
    1.32  fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
    1.33    let
    1.34 -    val _ = writeln "  Proving the introduction rules...";
    1.35 +    val _ = message "  Proving the introduction rules...";
    1.36  
    1.37      val unfold = standard (mono RS (fp_def RS
    1.38        (if coind then def_gfp_Tarski else def_lfp_Tarski)));
    1.39 @@ -261,7 +265,7 @@
    1.40  
    1.41  fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
    1.42    let
    1.43 -    val _ = writeln "  Proving the elimination rules...";
    1.44 +    val _ = message "  Proving the elimination rules...";
    1.45  
    1.46      val rules1 = [CollectE, disjE, make_elim vimageD];
    1.47      val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
    1.48 @@ -309,7 +313,7 @@
    1.49  fun prove_indrule cs cTs sumT rec_const params intr_ts mono
    1.50      fp_def rec_sets_defs thy =
    1.51    let
    1.52 -    val _ = writeln "  Proving the induction rule...";
    1.53 +    val _ = message "  Proving the induction rule...";
    1.54  
    1.55      val sign = sign_of thy;
    1.56  
    1.57 @@ -377,7 +381,7 @@
    1.58  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    1.59      intr_ts monos con_defs thy params paramTs cTs cnames =
    1.60    let
    1.61 -    val _ = if verbose then writeln ("Proofs for " ^
    1.62 +    val _ = if verbose then message ("Proofs for " ^
    1.63        (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
    1.64  
    1.65      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
    1.66 @@ -484,7 +488,7 @@
    1.67  fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
    1.68      intr_ts monos con_defs thy params paramTs cTs cnames =
    1.69    let
    1.70 -    val _ = if verbose then writeln ("Adding axioms for " ^
    1.71 +    val _ = if verbose then message ("Adding axioms for " ^
    1.72        (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
    1.73  
    1.74      val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;