haftmann@28213: theory Setup haftmann@39066: imports haftmann@39066: Complex_Main haftmann@46517: "~~/src/HOL/Library/Dlist" haftmann@46517: "~~/src/HOL/Library/RBT" haftmann@46517: "~~/src/HOL/Library/Mapping" haftmann@51162: "~~/src/HOL/Library/IArray" haftmann@28213: begin haftmann@28213: wenzelm@48951: ML_file "../antiquote_setup.ML" wenzelm@48951: ML_file "../more_antiquote.ML" wenzelm@48891: wenzelm@61143: no_syntax (output) wenzelm@61143: "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) wenzelm@61143: "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) wenzelm@61143: wenzelm@61143: syntax (output) wenzelm@61143: "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) wenzelm@61143: "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) haftmann@38503: haftmann@59324: declare [[default_code_width = 74]] haftmann@34071: wenzelm@42669: declare [[names_unique = false]] haftmann@28213: haftmann@28213: end