author  wenzelm 
Wed, 08 Oct 2008 19:20:29 +0200  
changeset 28529  7ff939586e83 
parent 24147  edc90be09ac1 
child 28866  30cd9d89a0fb 
permissions  rwrr 
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 metatheory*) 

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"]; 