# HG changeset patch
# User huffman
# Date 1240410013 25200
# Node ID e55eed7d9b5547189c205c7a6112ced1d138d18a
# Parent  ac7e90792089c4a9dcdeda1048e32924c82a6c20
add module signature for domain_theorems.ML

diff -r ac7e90792089 -r e55eed7d9b55 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 22 07:12:21 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 22 07:20:13 2009 -0700
@@ -8,7 +8,14 @@
 
 val HOLCF_ss = @{simpset};
 
-structure Domain_Theorems = struct
+signature DOMAIN_THEOREMS =
+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;
+end;
+
+structure Domain_Theorems : DOMAIN_THEOREMS =
+struct
 
 val quiet_mode = ref false;
 val trace_domain = ref false;