src/HOL/UNITY/ROOT.ML
author paulson
Wed May 26 10:15:03 1999 +0200 (1999-05-26)
changeset 6730 fa1f63249077
parent 6536 281d44905cab
child 6818 852f9ed01a53
permissions -rw-r--r--
new theories Follows and ListOrder
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
wenzelm@6349
     9
writeln"Root file for HOL/UNITY";
paulson@4776
    10
paulson@4776
    11
set proof_timing;
paulson@5648
    12
wenzelm@6216
    13
add_path "../Lex";	(*to find Prefix.thy*)
paulson@6012
    14
paulson@5648
    15
time_use_thy"UNITY";
paulson@4776
    16
time_use_thy "Deadlock";
paulson@4776
    17
time_use_thy "WFair";
paulson@4776
    18
time_use_thy "Common";
paulson@4776
    19
time_use_thy "Network";
paulson@4776
    20
time_use_thy "Token";
paulson@4776
    21
time_use_thy "Channel";
paulson@4776
    22
time_use_thy "Mutex";
paulson@4776
    23
time_use_thy "FP";
paulson@4776
    24
time_use_thy "Reach";
paulson@5253
    25
time_use_thy "Handshake";
paulson@5357
    26
time_use_thy "Lift";
paulson@5620
    27
time_use_thy "Comp";
paulson@6730
    28
(*Allocator example*)
paulson@5648
    29
time_use_thy "Client";
paulson@6295
    30
time_use_thy "Extend";
paulson@6295
    31
time_use_thy "PPROD";
paulson@6730
    32
time_use_thy "Follows";
paulson@5430
    33
wenzelm@6216
    34
add_path "../Auth";	(*to find Public.thy*)
paulson@5430
    35
use_thy"NSP_Bad";
wenzelm@6216
    36
wenzelm@6216
    37
reset_path ();