|
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;
|
|
5648
|
13 |
|
|
|
14 |
loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*)
|
|
|
15 |
time_use_thy"UNITY";
|
|
|
16 |
|
|
4776
|
17 |
time_use_thy "Deadlock";
|
|
|
18 |
time_use_thy "WFair";
|
|
|
19 |
time_use_thy "Common";
|
|
|
20 |
time_use_thy "Network";
|
|
|
21 |
time_use_thy "Token";
|
|
|
22 |
time_use_thy "Channel";
|
|
|
23 |
time_use_thy "Mutex";
|
|
|
24 |
time_use_thy "FP";
|
|
|
25 |
time_use_thy "Reach";
|
|
5253
|
26 |
time_use_thy "Handshake";
|
|
5357
|
27 |
time_use_thy "Lift";
|
|
5620
|
28 |
time_use_thy "Comp";
|
|
5648
|
29 |
time_use_thy "Client";
|
|
5430
|
30 |
|
|
5620
|
31 |
loadpath := "../Auth" :: !loadpath; (*to find Public.thy*)
|
|
5430
|
32 |
use_thy"NSP_Bad";
|