src/HOL/UNITY/ROOT.ML
author paulson
Fri Jan 05 10:15:48 2001 +0100 (2001-01-05)
changeset 10782 ddb433987557
parent 10265 4e004b548049
child 11193 851c90b23a9e
permissions -rw-r--r--
new examples by Sidi Ehmety
     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 time_use_thy "UNITY";
    10 time_use_thy "Deadlock";
    11 time_use_thy "WFair";
    12 time_use_thy "Common";
    13 time_use_thy "Network";
    14 time_use_thy "Token";
    15 time_use_thy "Channel";
    16 time_use_thy "Mutex";
    17 time_use_thy "FP";
    18 time_use_thy "Reach";
    19 time_use_thy "Handshake";
    20 time_use_thy "Lift";
    21 time_use_thy "Comp";
    22 time_use_thy "Reachability";
    23 
    24 (*Universal properties examples*)
    25 time_use_thy "Counter";
    26 time_use_thy "Counterc";
    27 time_use_thy "Priority";
    28 
    29 (*Allocator example*)
    30 time_use_thy "PPROD";
    31 time_use_thy "TimerArray";
    32 
    33 time_use_thy "Alloc";
    34 time_use_thy "AllocImpl";
    35 time_use_thy "Client";
    36 
    37 time_use_thy "ELT";  (*obsolete*)
    38 
    39 with_path "../Auth"  (*to find Public.thy*)
    40   time_use_thy"NSP_Bad";