author | huffman |
Tue, 12 May 2009 10:40:09 -0700 | |
changeset 31160 | 2823f1b6b860 |
parent 31120 | fc654c95c29e |
child 31161 | a27d4254ff4c |
--- 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 =