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 {*