src/HOL/UNITY/ROOT.ML
author wenzelm
Fri Aug 03 20:19:41 2007 +0200 (2007-08-03)
changeset 24147 edc90be09ac1
parent 21633 d1cb78244e30
child 28529 7ff939586e83
permissions -rw-r--r--
misc cleanup of ML bindings (for multihreading);
     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 quick_and_dirty true
    47   use_thy "Comp/Alloc";
    48 
    49 use_thys ["Comp/AllocImpl", "Comp/Client"];