no_document for Infinite_Set in HOLCF
authorhuffman
Sat, 13 Mar 2010 09:32:19 -0800
changeset 35768 cff6dfae284a
parent 35763 765f8adf10f9
child 35769 500c32e5fadc
no_document for Infinite_Set in HOLCF
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"];