--- a/src/HOL/Tools/typedef_package.ML Tue Oct 20 16:36:40 1998 +0200
+++ b/src/HOL/Tools/typedef_package.ML Tue Oct 20 16:37:02 1998 +0200
@@ -7,6 +7,7 @@
signature TYPEDEF_PACKAGE =
sig
+ val quiet_mode: bool ref
val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
val prove_nonempty: cterm -> thm list -> tactic option -> thm
val add_typedef: string -> bstring * string list * mixfix ->
@@ -39,6 +40,12 @@
(** type definitions **)
+(* messages *)
+
+val quiet_mode = ref false;
+fun message s = if ! quiet_mode then () else writeln s;
+
+
(* prove non-emptyness of a set *) (*exception ERROR*)
val is_def = Logic.is_equals o #prop o rep_thm;
@@ -123,7 +130,7 @@
if null errs then ()
else error (cat_lines errs);
- writeln("Proving nonemptiness of " ^ quote name ^ " ...");
+ message ("Proving nonemptiness of " ^ quote name ^ " ...");
prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
thy