| author | wenzelm | 
| Thu, 03 May 2012 13:17:15 +0200 | |
| changeset 47865 | 6ea205a4d7fd | 
| parent 35762 | af3ff2ba4c54 | 
| permissions | -rw-r--r-- | 
| 23912 | 1  | 
(* Title: ZF/UNITY/ROOT.ML  | 
| 11479 | 2  | 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory  | 
3  | 
Copyright 1998 University of Cambridge  | 
|
4  | 
||
| 23912 | 5  | 
ZF/UNITY proofs.  | 
| 11479 | 6  | 
*)  | 
7  | 
||
| 23912 | 8  | 
use_thys [  | 
9  | 
(*Simple examples: no composition*)  | 
|
10  | 
"Mutex",  | 
|
| 14052 | 11  | 
|
| 23912 | 12  | 
(*Basic meta-theory*)  | 
13  | 
"Guar",  | 
|
| 11479 | 14  | 
|
| 23912 | 15  | 
(*Prefix relation; the Allocator example*)  | 
16  | 
"Distributor", "Merge", "ClientImpl", "AllocImpl"  | 
|
17  | 
];  |