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
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@11193
    27
time_use_thy "Comp/Handshake";
paulson@9112
    28
paulson@10782
    29
(*Universal properties examples*)
paulson@11193
    30
time_use_thy "Comp/Counter";
paulson@11193
    31
time_use_thy "Comp/Counterc";
paulson@11193
    32
time_use_thy "Comp/Priority";
paulson@10782
    33
paulson@11193
    34
time_use_thy "Comp/TimerArray";
paulson@9112
    35
paulson@13790
    36
(*Allocator example*)
paulson@11193
    37
time_use_thy "Comp/Alloc";
paulson@11193
    38
time_use_thy "Comp/AllocImpl";
paulson@11193
    39
time_use_thy "Comp/Client";
paulson@8987
    40
paulson@8987
    41
time_use_thy "ELT";  (*obsolete*)