src/HOL/UNITY/ROOT.ML
author paulson
Mon Sep 07 10:43:31 1998 +0200 (1998-09-07)
changeset 5430 4a179dba527a
parent 5357 6efb2b87610c
child 5620 3ac11c4af76a
permissions -rw-r--r--
New UNITY theory, the N-S protocol
     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 time_use_thy "Deadlock";
    14 time_use_thy "WFair";
    15 time_use_thy "Common";
    16 time_use_thy "Network";
    17 time_use_thy "Token";
    18 time_use_thy "Channel";
    19 time_use_thy "Mutex";
    20 time_use_thy "FP";
    21 time_use_thy "Reach";
    22 time_use_thy "Handshake";
    23 time_use_thy "Lift";
    24 
    25 loadpath := "../Auth" :: !loadpath;  (*necessary to find the Auth theories*)
    26 use_thy"NSP_Bad";