src/HOL/UNITY/ROOT.ML
author wenzelm
Mon Dec 04 00:06:59 2006 +0100 (2006-12-04)
changeset 21633 d1cb78244e30
parent 14203 97df98601d23
child 24147 edc90be09ac1
permissions -rw-r--r--
theory Alloc no longer works -- quick_and_dirty;
     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 (*Basic meta-theory*)
    10 time_use_thy "UNITY_Main";
    11 
    12 (*Simple examples: no composition*)
    13 time_use_thy "Simple/Deadlock";
    14 time_use_thy "Simple/Common";
    15 time_use_thy "Simple/Network";
    16 time_use_thy "Simple/Token";
    17 time_use_thy "Simple/Channel";
    18 time_use_thy "Simple/Lift";
    19 time_use_thy "Simple/Mutex";
    20 time_use_thy "Simple/Reach";
    21 time_use_thy "Simple/Reachability";
    22 
    23 (*Verifying security protocols using UNITY*)
    24 with_path "../Auth" (no_document use_thy) "Public";
    25 with_path "../Auth" time_use_thy "Simple/NSP_Bad";
    26 
    27 (*Example of composition*)
    28 time_use_thy "Comp/Handshake";
    29 
    30 (*Universal properties examples*)
    31 time_use_thy "Comp/Counter";
    32 time_use_thy "Comp/Counterc";
    33 time_use_thy "Comp/Priority";
    34 
    35 time_use_thy "Comp/TimerArray";
    36 
    37 (*Allocator example*)
    38 (* FIXME some parts no longer work -- had been commented out for a long time *)
    39 setmp quick_and_dirty true
    40   time_use_thy "Comp/Alloc";
    41 time_use_thy "Comp/AllocImpl";
    42 time_use_thy "Comp/Client";
    43 
    44 time_use_thy "ELT";  (*obsolete*)