author | berghofe |
Thu, 06 Sep 2007 11:41:04 +0200 | |
changeset 24535 | d458d44639fc |
parent 24534 | 09b9a47904b7 |
child 24536 | fe33524ee721 |
--- a/src/HOL/Lambda/ROOT.ML Thu Sep 06 11:39:43 2007 +0200 +++ b/src/HOL/Lambda/ROOT.ML Thu Sep 06 11:41:04 2007 +0200 @@ -8,7 +8,7 @@ proofs := 2; no_document use_thys ["Accessible_Part", "Pretty_Int"]; -use_thys ["Eta", "StrongNorm"]; +use_thys ["Eta", "StrongNorm", "Standardization"]; if HOL_proofs < 2 then warning "HOL proof terms required for running theory WeakNorm" else use_thy "WeakNorm";