author | wenzelm |
Mon, 24 Oct 2016 14:05:22 +0200 | |
changeset 64371 | 213cf4215b40 |
parent 61670 | 301e0b4ecd45 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Setup |
39066 | 2 |
imports |
3 |
Complex_Main |
|
46517 | 4 |
"~~/src/HOL/Library/Dlist" |
5 |
"~~/src/HOL/Library/RBT" |
|
6 |
"~~/src/HOL/Library/Mapping" |
|
51162 | 7 |
"~~/src/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 |