--- a/src/HOLCF/Representable.thy Tue Mar 02 17:34:03 2010 -0800
+++ b/src/HOLCF/Representable.thy Tue Mar 02 18:16:28 2010 -0800
@@ -8,7 +8,6 @@
imports Algebraic Universal Ssum Sprod One Fixrec
uses
("Tools/repdef.ML")
- ("Tools/holcf_library.ML")
("Tools/Domain/domain_take_proofs.ML")
("Tools/Domain/domain_isomorphism.ML")
begin
@@ -778,7 +777,6 @@
subsection {* Constructing Domain Isomorphisms *}
-use "Tools/holcf_library.ML"
use "Tools/Domain/domain_take_proofs.ML"
use "Tools/Domain/domain_isomorphism.ML"