src/HOL/UNITY/ROOT.ML
author paulson
Mon Mar 05 15:25:11 2001 +0100 (2001-03-05)
changeset 11193 851c90b23a9e
parent 10782 ddb433987557
child 13785 e2fcd88be55d
permissions -rw-r--r--
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson@4776
     1
(*  Title:      HOL/UNITY/ROOT
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Root file for UNITY proofs.
paulson@4776
     7
*)
paulson@4776
     8
paulson@11193
     9
(*Basic meta-theory*)
paulson@11193
    10
time_use_thy "FP";
paulson@4776
    11
time_use_thy "WFair";
paulson@11193
    12
paulson@11193
    13
(*Simple examples: no composition*)
paulson@11193
    14
time_use_thy "Simple/Deadlock";
paulson@11193
    15
time_use_thy "Simple/Common";
paulson@11193
    16
time_use_thy "Simple/Network";
paulson@11193
    17
time_use_thy "Simple/Token";
paulson@11193
    18
time_use_thy "Simple/Channel";
paulson@11193
    19
time_use_thy "Simple/Lift";
paulson@11193
    20
time_use_thy "Simple/Mutex";
paulson@11193
    21
time_use_thy "Simple/Reach";
paulson@11193
    22
time_use_thy "Simple/Reachability";
paulson@11193
    23
paulson@11193
    24
with_path "../Auth"  (*to find Public.thy*)
paulson@11193
    25
  time_use_thy"Simple/NSP_Bad";
paulson@11193
    26
paulson@11193
    27
(*Example of composition*)
paulson@5620
    28
time_use_thy "Comp";
paulson@11193
    29
time_use_thy "Comp/Handshake";
paulson@9112
    30
paulson@10782
    31
(*Universal properties examples*)
paulson@11193
    32
time_use_thy "Comp/Counter";
paulson@11193
    33
time_use_thy "Comp/Counterc";
paulson@11193
    34
time_use_thy "Comp/Priority";
paulson@10782
    35
paulson@6730
    36
(*Allocator example*)
paulson@6295
    37
time_use_thy "PPROD";
paulson@11193
    38
time_use_thy "Comp/TimerArray";
paulson@9112
    39
paulson@11193
    40
time_use_thy "Comp/Alloc";
paulson@11193
    41
time_use_thy "Comp/AllocImpl";
paulson@11193
    42
time_use_thy "Comp/Client";
paulson@8987
    43
paulson@8987
    44
time_use_thy "ELT";  (*obsolete*)