src/HOLCF/Domain.thy

 theory Domain
 imports Ssum Sprod Up One Tr Fixrec Representable
 uses
   ("Tools/cont_consts.ML")
   ("Tools/cont_proc.ML")
+  ("Tools/Domain/domain_constructors.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")

 lemmas con_eq_iff_rules =
   sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
 
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"
+use "Tools/Domain/domain_constructors.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"