author | wenzelm |
Wed, 08 Oct 2008 19:20:29 +0200 | |
changeset 28529 | 7ff939586e83 |
parent 24147 | edc90be09ac1 |
child 28866 | 30cd9d89a0fb |
permissions | -rw-r--r-- |
4776 | 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 |
||
24147 | 9 |
(*Verifying security protocols using UNITY*) |
10 |
no_document use_thy "../Auth/Public"; |
|
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
10782
diff
changeset
|
11 |
|
24147 | 12 |
use_thys [ |
13 |
(*Basic meta-theory*) |
|
14 |
"UNITY_Main", |
|
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
10782
diff
changeset
|
15 |
|
24147 | 16 |
(*Simple examples: no composition*) |
17 |
"Simple/Deadlock", |
|
18 |
"Simple/Common", |
|
19 |
"Simple/Network", |
|
20 |
"Simple/Token", |
|
21 |
"Simple/Channel", |
|
22 |
"Simple/Lift", |
|
23 |
"Simple/Mutex", |
|
24 |
"Simple/Reach", |
|
25 |
"Simple/Reachability", |
|
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
10782
diff
changeset
|
26 |
|
24147 | 27 |
(*Verifying security protocols using UNITY*) |
28 |
"Simple/NSP_Bad", |
|
9112 | 29 |
|
24147 | 30 |
(*Example of composition*) |
31 |
"Comp/Handshake", |
|
10782 | 32 |
|
24147 | 33 |
(*Universal properties examples*) |
34 |
"Comp/Counter", |
|
35 |
"Comp/Counterc", |
|
36 |
"Comp/Priority", |
|
37 |
||
38 |
"Comp/TimerArray", |
|
39 |
||
40 |
(*obsolete*) |
|
41 |
"ELT" |
|
42 |
]; |
|
9112 | 43 |
|
13790 | 44 |
(*Allocator example*) |
21633 | 45 |
(* FIXME some parts no longer work -- had been commented out for a long time *) |
28529
7ff939586e83
setmp_noncritical makes it work with future scheduler;
wenzelm
parents:
24147
diff
changeset
|
46 |
setmp_noncritical quick_and_dirty true |
24147 | 47 |
use_thy "Comp/Alloc"; |
8987 | 48 |
|
24147 | 49 |
use_thys ["Comp/AllocImpl", "Comp/Client"]; |