src/HOL/UNITY/ROOT.ML
changeset 33615 261abc2e3155
parent 32624 3dec57ec3473
child 41892 2386fb64feaf
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
     1.3 @@ -1,13 +1,12 @@
     1.4  (*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6 -
     1.7  *)
     1.8  
     1.9  (*Verifying security protocols using UNITY*)
    1.10 -no_document use_thy "../Auth/Public";
    1.11 +no_document use_thys ["../Auth/Public"];
    1.12  
    1.13 -(*Basic meta-theory*)
    1.14 -use_thy "UNITY_Main";
    1.15 +use_thys [
    1.16 +  "UNITY_Main",     (*Basic meta-theory*)
    1.17 +  "UNITY_Examples"  (*Examples*)
    1.18 +];
    1.19  
    1.20 -(*Examples*)
    1.21 -use_thy "UNITY_Examples";