# HG changeset patch
# User huffman
# Date 1267826725 28800
# Node ID 49a02dab35ed1d13ddd3471af4508e77509a773e
# Parent  1785d387627a3a3d665a92473d3a42868d7efe9d
add comment

diff -r 1785d387627a -r 49a02dab35ed src/HOLCF/Representable.thy
--- 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"