src/HOL/UNITY/ROOT.ML
changeset 32624 3dec57ec3473
parent 28866 30cd9d89a0fb
child 33615 261abc2e3155
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Mon Sep 21 10:58:25 2009 +0200
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Mon Sep 21 12:22:53 2009 +0200
     1.3 @@ -1,50 +1,13 @@
     1.4 -(*  Title:      HOL/UNITY/ROOT
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1998  University of Cambridge
     1.9  
    1.10 -Root file for UNITY proofs.
    1.11  *)
    1.12  
    1.13  (*Verifying security protocols using UNITY*)
    1.14  no_document use_thy "../Auth/Public";
    1.15  
    1.16 -use_thys [
    1.17 -  (*Basic meta-theory*)
    1.18 -  "UNITY_Main",
    1.19 -
    1.20 -  (*Simple examples: no composition*)
    1.21 -  "Simple/Deadlock",
    1.22 -  "Simple/Common",
    1.23 -  "Simple/Network",
    1.24 -  "Simple/Token",
    1.25 -  "Simple/Channel",
    1.26 -  "Simple/Lift",
    1.27 -  "Simple/Mutex",
    1.28 -  "Simple/Reach",
    1.29 -  "Simple/Reachability",
    1.30 -
    1.31 -  (*Verifying security protocols using UNITY*)
    1.32 -  "Simple/NSP_Bad",
    1.33 +(*Basic meta-theory*)
    1.34 +use_thy "UNITY_Main";
    1.35  
    1.36 -  (*Example of composition*)
    1.37 -  "Comp/Handshake",
    1.38 -
    1.39 -  (*Universal properties examples*)
    1.40 -  "Comp/Counter",
    1.41 -  "Comp/Counterc",
    1.42 -  "Comp/Priority",
    1.43 -
    1.44 -  "Comp/TimerArray",
    1.45 -  "Comp/Progress",
    1.46 -
    1.47 -  (*obsolete*)
    1.48 -  "ELT"
    1.49 -];
    1.50 -
    1.51 -(*Allocator example*)
    1.52 -(* FIXME some parts no longer work -- had been commented out for a long time *)
    1.53 -setmp_noncritical quick_and_dirty true
    1.54 -  use_thy "Comp/Alloc";
    1.55 -
    1.56 -use_thys ["Comp/AllocImpl", "Comp/Client"];
    1.57 +(*Examples*)
    1.58 +use_thy "UNITY_Examples";