src/HOLCF/ROOT.ML
changeset 33615 261abc2e3155
parent 29921 3d50e96bcd6b
child 35707 44936737902d
     1.1 --- a/src/HOLCF/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     1.3 @@ -1,10 +1,9 @@
     1.4  (*  Title:      HOLCF/ROOT.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Franz Regensburger
     1.7  
     1.8  HOLCF -- a semantic extension of HOL by the LCF logic.
     1.9  *)
    1.10  
    1.11 -no_document use_thy "Nat_Int_Bij";
    1.12 +no_document use_thys ["Nat_Int_Bij"];
    1.13  
    1.14 -use_thy "HOLCF";
    1.15 +use_thys ["HOLCF"];