src/HOL/Lambda/ROOT.ML
changeset 9115 67409447f788
parent 9000 c20d58286a51
child 10264 ef384b242d09
     1.1 --- a/src/HOL/Lambda/ROOT.ML	Fri Jun 23 12:24:37 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Jun 23 12:28:09 2000 +0200
     1.3 @@ -6,4 +6,4 @@
     1.4  
     1.5  time_use_thy "Eta";
     1.6  with_path "../Induct" time_use_thy "Acc";
     1.7 -time_use_thy "InductTermi";
     1.8 +time_use_thy "Type";