src/HOL/UNITY/ROOT.ML
author paulson
Wed Jan 29 11:02:08 2003 +0100 (2003-01-29)
changeset 13790 8d7e9fce8c50
parent 13785 e2fcd88be55d
child 13821 0fd39aa77095
permissions -rw-r--r--
converting UNITY to 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/Handshake";
    28 
    29 (*Universal properties examples*)
    30 time_use_thy "Comp/Counter";
    31 time_use_thy "Comp/Counterc";
    32 time_use_thy "Comp/Priority";
    33 
    34 time_use_thy "Comp/TimerArray";
    35 
    36 (*Allocator example*)
    37 time_use_thy "Comp/Alloc";
    38 time_use_thy "Comp/AllocImpl";
    39 time_use_thy "Comp/Client";
    40 
    41 time_use_thy "ELT";  (*obsolete*)