src/HOL/Lambda/ROOT.ML
changeset 13031 3f7824dd8ddf
parent 11943 a9672446b45f
child 13550 5a176b8dda84
     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";