author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 61670 | 301e0b4ecd45 |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Setup |
39066 | 2 |
imports |
3 |
Complex_Main |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
61670
diff
changeset
|
4 |
"HOL-Library.Dlist" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
61670
diff
changeset
|
5 |
"HOL-Library.RBT" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
61670
diff
changeset
|
6 |
"HOL-Library.Mapping" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
61670
diff
changeset
|
7 |
"HOL-Library.IArray" |
28213 | 8 |
begin |
9 |
||
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48891
diff
changeset
|
10 |
ML_file "../antiquote_setup.ML" |
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48891
diff
changeset
|
11 |
ML_file "../more_antiquote.ML" |
48891 | 12 |
|
61143 | 13 |
no_syntax (output) |
14 |
"_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) |
|
15 |
"_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) |
|
16 |
||
17 |
syntax (output) |
|
18 |
"_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
|
19 |
"_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) |
|
38503 | 20 |
|
59324 | 21 |
declare [[default_code_width = 74]] |
34071 | 22 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42358
diff
changeset
|
23 |
declare [[names_unique = false]] |
28213 | 24 |
|
25 |
end |