src/HOLCF/Domain.thy

 
 header {* Domain package *}
 
 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
 
 

 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
   by rule auto
 
 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