src/HOL/UNITY/ROOT.ML
author paulson
Fri Jan 24 14:06:49 2003 +0100 (2003-01-24)
changeset 13785 e2fcd88be55d
parent 11193 851c90b23a9e
child 13790 8d7e9fce8c50
permissions -rw-r--r--
Partial conversion of UNITY to Isar new-style theories
     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 (*Basic meta-theory*)
    10 time_use_thy "UNITY_Main";
    11 
    12 (*Simple examples: no composition*)
    13 time_use_thy "Simple/Deadlock";
    14 time_use_thy "Simple/Common";
    15 time_use_thy "Simple/Network";
    16 time_use_thy "Simple/Token";
    17 time_use_thy "Simple/Channel";
    18 time_use_thy "Simple/Lift";
    19 time_use_thy "Simple/Mutex";
    20 time_use_thy "Simple/Reach";
    21 time_use_thy "Simple/Reachability";
    22 
    23 with_path "../Auth"  (*to find Public.thy*)
    24   time_use_thy"Simple/NSP_Bad";
    25 
    26 (*Example of composition*)
    27 time_use_thy "Comp";
    28 time_use_thy "Comp/Handshake";
    29 
    30 (*Universal properties examples*)
    31 time_use_thy "Comp/Counter";
    32 time_use_thy "Comp/Counterc";
    33 time_use_thy "Comp/Priority";
    34 
    35 (*Allocator example*)
    36 time_use_thy "PPROD";
    37 time_use_thy "Comp/TimerArray";
    38 
    39 time_use_thy "Comp/Alloc";
    40 time_use_thy "Comp/AllocImpl";
    41 time_use_thy "Comp/Client";
    42 
    43 time_use_thy "ELT";  (*obsolete*)