--- a/src/HOLCF/Representable.thy Fri Mar 05 13:56:04 2010 -0800
+++ b/src/HOLCF/Representable.thy Fri Mar 05 14:05:25 2010 -0800
@@ -14,6 +14,12 @@
subsection {* Preliminaries: Take proofs *}
+text {*
+ This section contains lemmas that are used in a module that supports
+ the domain isomorphism package; the module contains proofs related
+ to take functions and the finiteness predicate.
+*}
+
lemma deflation_abs_rep:
fixes abs and rep and d
assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"