src/HOL/Nominal/ROOT.ML
changeset 33615 261abc2e3155
parent 24584 01e83ffa6c54
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Nominal/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     1.2 +++ b/src/HOL/Nominal/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     1.3 @@ -1,9 +1,8 @@
     1.4  (*  Title:      HOL/Nominal/ROOT.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer and Christian Urban, TU Muenchen
     1.7  
     1.8  The nominal datatype package.
     1.9  *)
    1.10  
    1.11 -no_document use_thy "Infinite_Set";
    1.12 -use_thy "Nominal";
    1.13 +no_document use_thys ["Infinite_Set"];
    1.14 +use_thys ["Nominal"];