# HG changeset patch
# User wenzelm
# Date 1015433319 -3600
# Node ID 3f7824dd8ddf6ddc82b630935c35800a558e196c
# Parent  5765aa72afac56248b07014bb3a928562c710d75
tuned;

diff -r 5765aa72afac -r 3f7824dd8ddf src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Wed Mar 06 17:48:08 2002 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Wed Mar 06 17:48:39 2002 +0100
@@ -7,5 +7,5 @@
 Syntax.ambiguity_level := 100;
 
 time_use_thy "Eta";
-time_use_thy "Accessible_Part";
+no_document time_use_thy "Accessible_Part";
 time_use_thy "Type";
diff -r 5765aa72afac -r 3f7824dd8ddf src/HOL/Lambda/document/root.tex
--- a/src/HOL/Lambda/document/root.tex	Wed Mar 06 17:48:08 2002 +0100
+++ b/src/HOL/Lambda/document/root.tex	Wed Mar 06 17:48:39 2002 +0100
@@ -28,14 +28,6 @@
 
 \parindent 0pt \parskip 0.5ex
 
-\input{Lambda}
-\input{Commutation}
-\input{ParRed}
-\input{Eta}
-\input{ListApplication}
-\input{ListOrder}
-\input{ListBeta}
-\input{InductTermi}
-\input{Type}
+\input{session}
 
 \end{document}