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
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@13785
    10
time_use_thy "UNITY_Main";
paulson@11193
    11
paulson@11193
    12
(*Simple examples: no composition*)
paulson@11193
    13
time_use_thy "Simple/Deadlock";
paulson@11193
    14
time_use_thy "Simple/Common";
paulson@11193
    15
time_use_thy "Simple/Network";
paulson@11193
    16
time_use_thy "Simple/Token";
paulson@11193
    17
time_use_thy "Simple/Channel";
paulson@11193
    18
time_use_thy "Simple/Lift";
paulson@11193
    19
time_use_thy "Simple/Mutex";
paulson@11193
    20
time_use_thy "Simple/Reach";
paulson@11193
    21
time_use_thy "Simple/Reachability";
paulson@11193
    22
paulson@11193
    23
with_path "../Auth"  (*to find Public.thy*)
paulson@11193
    24
  time_use_thy"Simple/NSP_Bad";
paulson@11193
    25
paulson@11193
    26
(*Example of composition*)
paulson@5620
    27
time_use_thy "Comp";
paulson@11193
    28
time_use_thy "Comp/Handshake";
paulson@9112
    29
paulson@10782
    30
(*Universal properties examples*)
paulson@11193
    31
time_use_thy "Comp/Counter";
paulson@11193
    32
time_use_thy "Comp/Counterc";
paulson@11193
    33
time_use_thy "Comp/Priority";
paulson@10782
    34
paulson@6730
    35
(*Allocator example*)
paulson@6295
    36
time_use_thy "PPROD";
paulson@11193
    37
time_use_thy "Comp/TimerArray";
paulson@9112
    38
paulson@11193
    39
time_use_thy "Comp/Alloc";
paulson@11193
    40
time_use_thy "Comp/AllocImpl";
paulson@11193
    41
time_use_thy "Comp/Client";
paulson@8987
    42
paulson@8987
    43
time_use_thy "ELT";  (*obsolete*)