--- 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";
--- 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}