src/HOLCF/Representable.thy
changeset 35514 a2cfa413eaab
parent 35490 63f8121c6585
child 35525 fa231b86cb1e
--- a/src/HOLCF/Representable.thy	Tue Mar 02 13:01:22 2010 -0800
+++ b/src/HOLCF/Representable.thy	Tue Mar 02 13:50:23 2010 -0800
@@ -9,6 +9,7 @@
 uses
   ("Tools/repdef.ML")
   ("Tools/holcf_library.ML")
+  ("Tools/Domain/domain_take_proofs.ML")
   ("Tools/Domain/domain_isomorphism.ML")
 begin
 
@@ -778,6 +779,7 @@
 subsection {* Constructing Domain Isomorphisms *}
 
 use "Tools/holcf_library.ML"
+use "Tools/Domain/domain_take_proofs.ML"
 use "Tools/Domain/domain_isomorphism.ML"
 
 setup {*