author | berghofe |
Mon, 06 Aug 2007 16:05:25 +0200 | |
changeset 24156 | 99e4722eceb1 |
parent 24155 | d86867645f4f |
child 24157 | 409cd6eaa7ea |
--- 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"