# HG changeset patch
# User berghofe
# Date 1189071664 -7200
# Node ID d458d44639fcd1be7b8a7ea91413f5c8ec0f2d55
# Parent  09b9a47904b785308ddf8feff67c863d1bc795fd
Added Standardization theory.

diff -r 09b9a47904b7 -r d458d44639fc src/HOL/Lambda/ROOT.ML
--- 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";