src/HOL/UNITY/ROOT.ML
author paulson
Fri Jun 23 10:34:51 2000 +0200 (2000-06-23)
changeset 9112 44fc37919579
parent 9000 c20d58286a51
child 10265 4e004b548049
permissions -rw-r--r--
added the AllocImpl example
paulson@4776
     1
(*  Title:      HOL/UNITY/ROOT
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Root file for UNITY proofs.
paulson@4776
     7
*)
paulson@4776
     8
paulson@6818
     9
time_use_thy "UNITY";
paulson@4776
    10
time_use_thy "Deadlock";
paulson@4776
    11
time_use_thy "WFair";
paulson@4776
    12
time_use_thy "Common";
paulson@4776
    13
time_use_thy "Network";
paulson@4776
    14
time_use_thy "Token";
paulson@4776
    15
time_use_thy "Channel";
paulson@4776
    16
time_use_thy "Mutex";
paulson@4776
    17
time_use_thy "FP";
paulson@4776
    18
time_use_thy "Reach";
paulson@5253
    19
time_use_thy "Handshake";
paulson@5357
    20
time_use_thy "Lift";
paulson@5620
    21
time_use_thy "Comp";
paulson@8987
    22
time_use_thy "Reachability";
paulson@9112
    23
paulson@6730
    24
(*Allocator example*)
paulson@6295
    25
time_use_thy "PPROD";
paulson@7513
    26
time_use_thy "TimerArray";
paulson@9112
    27
paulson@9112
    28
add_path "../Induct";
paulson@9112
    29
time_use_thy "Alloc";
paulson@9112
    30
time_use_thy "AllocImpl";
paulson@8987
    31
time_use_thy "Client";
paulson@8987
    32
paulson@8987
    33
time_use_thy "ELT";  (*obsolete*)
paulson@5430
    34
wenzelm@9000
    35
with_path "../Auth"  (*to find Public.thy*)
wenzelm@9000
    36
  time_use_thy"NSP_Bad";