# HG changeset patch
# User huffman
# Date 1268501539 28800
# Node ID cff6dfae284a3e17e60e98dbeddb6c84225d0214
# Parent  765f8adf10f9c5ff04680ea5b6be9055ccfba08e
no_document for Infinite_Set in HOLCF

diff -r 765f8adf10f9 -r cff6dfae284a src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Sat Mar 13 17:19:12 2010 +0100
+++ b/src/HOLCF/ROOT.ML	Sat Mar 13 09:32:19 2010 -0800
@@ -4,6 +4,6 @@
 HOLCF -- a semantic extension of HOL by the LCF logic.
 *)
 
-no_document use_thys ["Nat_Bijection"];
+no_document use_thys ["Nat_Bijection", "Infinite_Set"];
 
 use_thys ["HOLCF"];