src/HOL/UNITY/ROOT.ML
changeset 24147 edc90be09ac1
parent 21633 d1cb78244e30
child 28529 7ff939586e83
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Fri Aug 03 16:28:25 2007 +0200
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Aug 03 20:19:41 2007 +0200
     1.3 @@ -6,39 +6,44 @@
     1.4  Root file for UNITY proofs.
     1.5  *)
     1.6  
     1.7 -(*Basic meta-theory*)
     1.8 -time_use_thy "UNITY_Main";
     1.9 +(*Verifying security protocols using UNITY*)
    1.10 +no_document use_thy "../Auth/Public";
    1.11  
    1.12 -(*Simple examples: no composition*)
    1.13 -time_use_thy "Simple/Deadlock";
    1.14 -time_use_thy "Simple/Common";
    1.15 -time_use_thy "Simple/Network";
    1.16 -time_use_thy "Simple/Token";
    1.17 -time_use_thy "Simple/Channel";
    1.18 -time_use_thy "Simple/Lift";
    1.19 -time_use_thy "Simple/Mutex";
    1.20 -time_use_thy "Simple/Reach";
    1.21 -time_use_thy "Simple/Reachability";
    1.22 +use_thys [
    1.23 +  (*Basic meta-theory*)
    1.24 +  "UNITY_Main",
    1.25  
    1.26 -(*Verifying security protocols using UNITY*)
    1.27 -with_path "../Auth" (no_document use_thy) "Public";
    1.28 -with_path "../Auth" time_use_thy "Simple/NSP_Bad";
    1.29 +  (*Simple examples: no composition*)
    1.30 +  "Simple/Deadlock",
    1.31 +  "Simple/Common",
    1.32 +  "Simple/Network",
    1.33 +  "Simple/Token",
    1.34 +  "Simple/Channel",
    1.35 +  "Simple/Lift",
    1.36 +  "Simple/Mutex",
    1.37 +  "Simple/Reach",
    1.38 +  "Simple/Reachability",
    1.39  
    1.40 -(*Example of composition*)
    1.41 -time_use_thy "Comp/Handshake";
    1.42 +  (*Verifying security protocols using UNITY*)
    1.43 +  "Simple/NSP_Bad",
    1.44  
    1.45 -(*Universal properties examples*)
    1.46 -time_use_thy "Comp/Counter";
    1.47 -time_use_thy "Comp/Counterc";
    1.48 -time_use_thy "Comp/Priority";
    1.49 +  (*Example of composition*)
    1.50 +  "Comp/Handshake",
    1.51  
    1.52 -time_use_thy "Comp/TimerArray";
    1.53 +  (*Universal properties examples*)
    1.54 +  "Comp/Counter",
    1.55 +  "Comp/Counterc",
    1.56 +  "Comp/Priority",
    1.57 +
    1.58 +  "Comp/TimerArray",
    1.59 +
    1.60 +  (*obsolete*)
    1.61 +  "ELT"
    1.62 +];
    1.63  
    1.64  (*Allocator example*)
    1.65  (* FIXME some parts no longer work -- had been commented out for a long time *)
    1.66  setmp quick_and_dirty true
    1.67 -  time_use_thy "Comp/Alloc";
    1.68 -time_use_thy "Comp/AllocImpl";
    1.69 -time_use_thy "Comp/Client";
    1.70 +  use_thy "Comp/Alloc";
    1.71  
    1.72 -time_use_thy "ELT";  (*obsolete*)
    1.73 +use_thys ["Comp/AllocImpl", "Comp/Client"];