|
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 |
|
|
|
9 |
HOL_build_completed; (*Make examples fail if HOL did*)
|
|
|
10 |
|
|
|
11 |
writeln"Root file for HOL/UNITY";
|
|
|
12 |
set proof_timing;
|
|
|
13 |
time_use_thy "Deadlock";
|
|
|
14 |
time_use_thy "WFair";
|
|
|
15 |
time_use_thy "Common";
|
|
|
16 |
time_use_thy "Network";
|
|
|
17 |
time_use_thy "Token";
|
|
|
18 |
time_use_thy "Channel";
|
|
|
19 |
time_use_thy "Mutex";
|
|
|
20 |
time_use_thy "FP";
|
|
|
21 |
time_use_thy "Reach";
|
|
5253
|
22 |
time_use_thy "Handshake";
|
|
5357
|
23 |
time_use_thy "Lift";
|
|
5430
|
24 |
|
|
|
25 |
loadpath := "../Auth" :: !loadpath; (*necessary to find the Auth theories*)
|
|
|
26 |
use_thy"NSP_Bad";
|