tuned;
authorwenzelm
Wed Mar 06 17:48:39 2002 +0100 (2002-03-06)
changeset 130313f7824dd8ddf
parent 13030 5765aa72afac
child 13032 1ec445c51931
tuned;
src/HOL/Lambda/ROOT.ML
src/HOL/Lambda/document/root.tex
     1.1 --- a/src/HOL/Lambda/ROOT.ML	Wed Mar 06 17:48:08 2002 +0100
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Wed Mar 06 17:48:39 2002 +0100
     1.3 @@ -7,5 +7,5 @@
     1.4  Syntax.ambiguity_level := 100;
     1.5  
     1.6  time_use_thy "Eta";
     1.7 -time_use_thy "Accessible_Part";
     1.8 +no_document time_use_thy "Accessible_Part";
     1.9  time_use_thy "Type";
     2.1 --- a/src/HOL/Lambda/document/root.tex	Wed Mar 06 17:48:08 2002 +0100
     2.2 +++ b/src/HOL/Lambda/document/root.tex	Wed Mar 06 17:48:39 2002 +0100
     2.3 @@ -28,14 +28,6 @@
     2.4  
     2.5  \parindent 0pt \parskip 0.5ex
     2.6  
     2.7 -\input{Lambda}
     2.8 -\input{Commutation}
     2.9 -\input{ParRed}
    2.10 -\input{Eta}
    2.11 -\input{ListApplication}
    2.12 -\input{ListOrder}
    2.13 -\input{ListBeta}
    2.14 -\input{InductTermi}
    2.15 -\input{Type}
    2.16 +\input{session}
    2.17  
    2.18  \end{document}