src/HOL/UNITY/ROOT.ML
author paulson
Mon Mar 05 15:25:11 2001 +0100 (2001-03-05)
changeset 11193 851c90b23a9e
parent 10782 ddb433987557
child 13785 e2fcd88be55d
permissions -rw-r--r--
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
     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 "FP";
    11 time_use_thy "WFair";
    12 
    13 (*Simple examples: no composition*)
    14 time_use_thy "Simple/Deadlock";
    15 time_use_thy "Simple/Common";
    16 time_use_thy "Simple/Network";
    17 time_use_thy "Simple/Token";
    18 time_use_thy "Simple/Channel";
    19 time_use_thy "Simple/Lift";
    20 time_use_thy "Simple/Mutex";
    21 time_use_thy "Simple/Reach";
    22 time_use_thy "Simple/Reachability";
    23 
    24 with_path "../Auth"  (*to find Public.thy*)
    25   time_use_thy"Simple/NSP_Bad";
    26 
    27 (*Example of composition*)
    28 time_use_thy "Comp";
    29 time_use_thy "Comp/Handshake";
    30 
    31 (*Universal properties examples*)
    32 time_use_thy "Comp/Counter";
    33 time_use_thy "Comp/Counterc";
    34 time_use_thy "Comp/Priority";
    35 
    36 (*Allocator example*)
    37 time_use_thy "PPROD";
    38 time_use_thy "Comp/TimerArray";
    39 
    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*)