--- a/src/HOLCF/Domain.thy Wed Apr 08 20:29:15 2009 +0200
+++ b/src/HOLCF/Domain.thy Fri Apr 10 11:35:21 2009 -0700
@@ -6,6 +6,14 @@
theory Domain
imports Ssum Sprod Up One Tr Fixrec
+uses
+ ("Tools/cont_consts.ML")
+ ("Tools/cont_proc.ML")
+ ("Tools/domain/domain_library.ML")
+ ("Tools/domain/domain_syntax.ML")
+ ("Tools/domain/domain_axioms.ML")
+ ("Tools/domain/domain_theorems.ML")
+ ("Tools/domain/domain_extender.ML")
begin
defaultsort pcpo
@@ -193,4 +201,15 @@
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
+
+subsection {* Installing the domain package *}
+
+use "Tools/cont_consts.ML"
+use "Tools/cont_proc.ML"
+use "Tools/domain/domain_library.ML"
+use "Tools/domain/domain_syntax.ML"
+use "Tools/domain/domain_axioms.ML"
+use "Tools/domain/domain_theorems.ML"
+use "Tools/domain/domain_extender.ML"
+
end