equal
deleted
inserted
replaced
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 |
13 |
|
14 add_path "../Lex"; (*to find Prefix.thy*) |
14 |
15 |
15 |
|
16 loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*) |
|
17 time_use_thy"UNITY"; |
16 time_use_thy"UNITY"; |
18 |
17 |
19 time_use_thy "Deadlock"; |
18 time_use_thy "Deadlock"; |
20 time_use_thy "WFair"; |
19 time_use_thy "WFair"; |
21 time_use_thy "Common"; |
20 time_use_thy "Common"; |
31 time_use_thy "Client"; |
30 time_use_thy "Client"; |
32 (** |
31 (** |
33 time_use_thy "PPX"; |
32 time_use_thy "PPX"; |
34 **) |
33 **) |
35 |
34 |
36 loadpath := "../Auth" :: !loadpath; (*to find Public.thy*) |
35 add_path "../Auth"; (*to find Public.thy*) |
37 use_thy"NSP_Bad"; |
36 use_thy"NSP_Bad"; |
|
37 |
|
38 reset_path (); |