export quiet_mode and trace_domain refs for domain package
authorhuffman
Tue, 12 May 2009 10:40:09 -0700
changeset 31160 2823f1b6b860
parent 31120 fc654c95c29e
child 31161 a27d4254ff4c
export quiet_mode and trace_domain refs for domain package
src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue May 12 17:32:50 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue May 12 10:40:09 2009 -0700
@@ -12,6 +12,8 @@
 sig
   val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
   val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+  val quiet_mode: bool ref;
+  val trace_domain: bool ref;
 end;
 
 structure Domain_Theorems :> DOMAIN_THEOREMS =