| changeset 30226 | 2f4684e2ea95 |
| parent 30202 | 2775062fd3a9 |
| child 30227 | 853abb4853cc |
| 30202:2775062fd3a9 | 30226:2f4684e2ea95 |
|---|---|
1 theory Setup |
|
2 imports Complex_Main |
|
3 uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML" |
|
4 begin |
|
5 |
|
6 ML {* no_document use_thys |
|
7 ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL", |
|
8 "~~/src/HOL/Decision_Procs/Ferrack"] *} |
|
9 |
|
10 ML_val {* Code_Target.code_width := 74 *} |
|
11 |
|
12 end |