author | haftmann |
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06) | |
changeset 64990 | c6a7de505796 |
parent 61670 | 301e0b4ecd45 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
haftmann@28213 | 1 |
theory Setup |
haftmann@39066 | 2 |
imports |
haftmann@39066 | 3 |
Complex_Main |
haftmann@46517 | 4 |
"~~/src/HOL/Library/Dlist" |
haftmann@46517 | 5 |
"~~/src/HOL/Library/RBT" |
haftmann@46517 | 6 |
"~~/src/HOL/Library/Mapping" |
haftmann@51162 | 7 |
"~~/src/HOL/Library/IArray" |
haftmann@28213 | 8 |
begin |
haftmann@28213 | 9 |
|
wenzelm@48951 | 10 |
ML_file "../antiquote_setup.ML" |
wenzelm@48951 | 11 |
ML_file "../more_antiquote.ML" |
wenzelm@48891 | 12 |
|
wenzelm@61143 | 13 |
no_syntax (output) |
wenzelm@61143 | 14 |
"_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) |
wenzelm@61143 | 15 |
"_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) |
wenzelm@61143 | 16 |
|
wenzelm@61143 | 17 |
syntax (output) |
wenzelm@61143 | 18 |
"_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) |
wenzelm@61143 | 19 |
"_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) |
haftmann@38503 | 20 |
|
haftmann@59324 | 21 |
declare [[default_code_width = 74]] |
haftmann@34071 | 22 |
|
wenzelm@42669 | 23 |
declare [[names_unique = false]] |
haftmann@28213 | 24 |
|
haftmann@28213 | 25 |
end |