| changeset 16121 | a80aa66d2271 |
| parent 15570 | 8d8c70b41bab |
| child 16417 | 9bc16273c2d4 |
| 16120:6a449deff8d9 | 16121:a80aa66d2271 |
|---|---|
5 *) |
5 *) |
6 header {* Definitions extending HOL as logical basis of Bali *} |
6 header {* Definitions extending HOL as logical basis of Bali *} |
7 |
7 |
8 theory Basis = Main: |
8 theory Basis = Main: |
9 |
9 |
10 ML_setup {* |
10 ML {* |
11 Unify.search_bound := 40; |
11 Unify.search_bound := 40; |
12 Unify.trace_bound := 40; |
12 Unify.trace_bound := 40; |
13 *} |
13 *} |
14 (*print_depth 100;*) |
14 (*print_depth 100;*) |
15 (*Syntax.ambiguity_level := 1;*) |
15 (*Syntax.ambiguity_level := 1;*) |