# HG changeset patch
# User berghofe
# Date 1186409125 -7200
# Node ID 99e4722eceb150dd376b50e2620760ccc7be61c5
# Parent  d86867645f4f938ba3b20e47231b30e47485e6c4
No document for Pretty_Int theory.

diff -r d86867645f4f -r 99e4722eceb1 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Mon Aug 06 11:45:39 2007 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Mon Aug 06 16:05:25 2007 +0200
@@ -7,7 +7,7 @@
 Syntax.ambiguity_level := 100;
 proofs := 2;
 
-no_document use_thy "Accessible_Part";
+no_document use_thys ["Accessible_Part", "Pretty_Int"];
 use_thys ["Eta", "StrongNorm"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"