changeset 22100 | 33d7468302bb |
parent 21676 | a45af03f6827 |
child 24104 | 719fbe4fb77f |
22099:5dc00ac4bd8e | 22100:33d7468302bb |
---|---|
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
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; |
|
10 |
9 |
11 use_thy "Eta"; |
10 use_thy "Eta"; |
12 no_document use_thy "Accessible_Part"; |
11 no_document use_thy "Accessible_Part"; |
13 use_thy "StrongNorm"; |
12 use_thy "StrongNorm"; |
14 if HOL_proofs < 2 then |
13 if HOL_proofs < 2 then |