src/HOL/UNITY/ROOT.ML
author paulson
Thu Dec 03 10:45:06 1998 +0100 (1998-12-03)
changeset 6012 1894bfc4aee9
parent 5899 13d4753079fe
child 6216 05d99c0bbfa0
permissions -rw-r--r--
Addition of the States component; parts of Comp not working
     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 HOL_build_completed;    (*Make examples fail if HOL did*)
    10 
    11 writeln"Root file for HOL/UNITY";
    12 set proof_timing;
    13 
    14 
    15 
    16 loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
    17 time_use_thy"UNITY";
    18 
    19 time_use_thy "Deadlock";
    20 time_use_thy "WFair";
    21 time_use_thy "Common";
    22 time_use_thy "Network";
    23 time_use_thy "Token";
    24 time_use_thy "Channel";
    25 time_use_thy "Mutex";
    26 time_use_thy "FP";
    27 time_use_thy "Reach";
    28 time_use_thy "Handshake";
    29 time_use_thy "Lift";
    30 time_use_thy "Comp";
    31 time_use_thy "Client";
    32 (**
    33 time_use_thy "PPX";
    34 **)
    35 
    36 loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
    37 use_thy"NSP_Bad";