src/HOL/UNITY/ROOT.ML
author paulson
Tue Sep 23 15:49:17 2003 +0200 (2003-09-23)
changeset 14203 97df98601d23
parent 13853 89131afa9f01
child 21633 d1cb78244e30
permissions -rw-r--r--
conversion of NSP_Bad to Isar script
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@14203
    23
(*Verifying security protocols using UNITY*)
paulson@14203
    24
with_path "../Auth" (no_document use_thy) "Public";
paulson@14203
    25
with_path "../Auth" time_use_thy "Simple/NSP_Bad";
paulson@11193
    26
paulson@11193
    27
(*Example of composition*)
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@11193
    35
time_use_thy "Comp/TimerArray";
paulson@9112
    36
paulson@13790
    37
(*Allocator example*)
paulson@11193
    38
time_use_thy "Comp/Alloc";
paulson@11193
    39
time_use_thy "Comp/AllocImpl";
paulson@11193
    40
time_use_thy "Comp/Client";
paulson@8987
    41
paulson@8987
    42
time_use_thy "ELT";  (*obsolete*)