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/Auth"; |
11 writeln"Root file for HOL/Auth"; |
12 proof_timing := true; |
12 proof_timing := true; |
13 goals_limit := 1; |
13 goals_limit := 1; |
14 |
|
15 (*New version of addss isn't ready--too slow*) |
|
16 val op addss = op unsafe_addss; |
|
17 |
14 |
18 (*Shared-key protocols*) |
15 (*Shared-key protocols*) |
19 time_use_thy "NS_Shared"; |
16 time_use_thy "NS_Shared"; |
20 time_use_thy "OtwayRees"; |
17 time_use_thy "OtwayRees"; |
21 time_use_thy "OtwayRees_AN"; |
18 time_use_thy "OtwayRees_AN"; |