equal
deleted
inserted
replaced
6 |
6 |
7 Syntax.ambiguity_level := 100; |
7 Syntax.ambiguity_level := 100; |
8 proofs := 2; |
8 proofs := 2; |
9 IsarOutput.modes := "no_brackets" :: !IsarOutput.modes; |
9 IsarOutput.modes := "no_brackets" :: !IsarOutput.modes; |
10 |
10 |
11 set timing; |
11 use_thy "Eta"; |
12 time_use_thy "Eta"; |
12 no_document use_thy "Accessible_Part"; |
13 no_document time_use_thy "Accessible_Part"; |
13 use_thy "StrongNorm"; |
14 time_use_thy "StrongNorm"; |
|
15 if HOL_proofs < 2 then |
14 if HOL_proofs < 2 then |
16 warning "HOL proof terms required for running theory WeakNorm" |
15 warning "HOL proof terms required for running theory WeakNorm" |
17 else time_use_thy "WeakNorm"; |
16 else use_thy "WeakNorm"; |