changeset 24994 | c385c4eabb3b |
parent 24535 | d458d44639fc |
child 25374 | 7657a081fcb4 |
--- a/src/HOL/Lambda/ROOT.ML Fri Oct 12 08:20:46 2007 +0200 +++ b/src/HOL/Lambda/ROOT.ML Fri Oct 12 08:21:09 2007 +0200 @@ -7,7 +7,7 @@ Syntax.ambiguity_level := 100; proofs := 2; -no_document use_thys ["Accessible_Part", "Pretty_Int"]; +no_document use_thys ["Accessible_Part", "Code_Integer"]; use_thys ["Eta", "StrongNorm", "Standardization"]; if HOL_proofs < 2 then warning "HOL proof terms required for running theory WeakNorm"