src/HOL/UNITY/ROOT.ML
author wenzelm
Wed Oct 08 19:20:29 2008 +0200 (2008-10-08)
changeset 28529 7ff939586e83
parent 24147 edc90be09ac1
child 28866 30cd9d89a0fb
permissions -rw-r--r--
setmp_noncritical makes it work with future scheduler;
     1 (*  Title:      HOL/UNITY/ROOT
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Root file for UNITY proofs.
     7 *)
     8 
     9 (*Verifying security protocols using UNITY*)
    10 no_document use_thy "../Auth/Public";
    11 
    12 use_thys [
    13   (*Basic meta-theory*)
    14   "UNITY_Main",
    15 
    16   (*Simple examples: no composition*)
    17   "Simple/Deadlock",
    18   "Simple/Common",
    19   "Simple/Network",
    20   "Simple/Token",
    21   "Simple/Channel",
    22   "Simple/Lift",
    23   "Simple/Mutex",
    24   "Simple/Reach",
    25   "Simple/Reachability",
    26 
    27   (*Verifying security protocols using UNITY*)
    28   "Simple/NSP_Bad",
    29 
    30   (*Example of composition*)
    31   "Comp/Handshake",
    32 
    33   (*Universal properties examples*)
    34   "Comp/Counter",
    35   "Comp/Counterc",
    36   "Comp/Priority",
    37 
    38   "Comp/TimerArray",
    39 
    40   (*obsolete*)
    41   "ELT"
    42 ];
    43 
    44 (*Allocator example*)
    45 (* FIXME some parts no longer work -- had been commented out for a long time *)
    46 setmp_noncritical quick_and_dirty true
    47   use_thy "Comp/Alloc";
    48 
    49 use_thys ["Comp/AllocImpl", "Comp/Client"];