src/HOL/UNITY/ROOT.ML
author paulson
Fri Feb 18 15:20:44 2000 +0100 (2000-02-18)
changeset 8251 9be357df93d4
parent 8128 3a5864b465e2
child 8314 463f63a9a7f2
permissions -rw-r--r--
New treatment of "guarantees" with polymorphic components and bijections.
Works EXCEPT FOR Alloc.
     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 writeln"Root file for HOL/UNITY";
    10 
    11 set proof_timing;
    12 
    13 time_use_thy "UNITY";
    14 time_use_thy "Deadlock";
    15 time_use_thy "WFair";
    16 time_use_thy "Common";
    17 time_use_thy "Network";
    18 time_use_thy "Token";
    19 time_use_thy "Channel";
    20 time_use_thy "Mutex";
    21 time_use_thy "FP";
    22 time_use_thy "Reach";
    23 time_use_thy "Handshake";
    24 time_use_thy "Lift";
    25 time_use_thy "Comp";
    26 (*Allocator example*)
    27 time_use_thy "Client";
    28 time_use_thy "Extend";
    29 time_use_thy "PPROD";
    30 time_use_thy "TimerArray";
    31 (**
    32 time_use_thy "Alloc";
    33 **)
    34 
    35 add_path "../Auth";	(*to find Public.thy*)
    36 use_thy"NSP_Bad";
    37 
    38 reset_path ();