equal
deleted
inserted
replaced
8 |
8 |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
10 |
10 |
11 writeln"Root file for HOL/UNITY"; |
11 writeln"Root file for HOL/UNITY"; |
12 set proof_timing; |
12 set proof_timing; |
|
13 |
|
14 loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*) |
|
15 time_use_thy"UNITY"; |
|
16 |
13 time_use_thy "Deadlock"; |
17 time_use_thy "Deadlock"; |
14 time_use_thy "WFair"; |
18 time_use_thy "WFair"; |
15 time_use_thy "Common"; |
19 time_use_thy "Common"; |
16 time_use_thy "Network"; |
20 time_use_thy "Network"; |
17 time_use_thy "Token"; |
21 time_use_thy "Token"; |
20 time_use_thy "FP"; |
24 time_use_thy "FP"; |
21 time_use_thy "Reach"; |
25 time_use_thy "Reach"; |
22 time_use_thy "Handshake"; |
26 time_use_thy "Handshake"; |
23 time_use_thy "Lift"; |
27 time_use_thy "Lift"; |
24 time_use_thy "Comp"; |
28 time_use_thy "Comp"; |
|
29 time_use_thy "Client"; |
25 |
30 |
26 loadpath := "../Auth" :: !loadpath; (*to find Public.thy*) |
31 loadpath := "../Auth" :: !loadpath; (*to find Public.thy*) |
27 use_thy"NSP_Bad"; |
32 use_thy"NSP_Bad"; |
28 |
|
29 loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*) |
|
30 use_thy"Client"; |
|