equal
deleted
inserted
replaced
1 theory Setup |
1 theory Setup |
2 imports Main "~~/src/HOL/Library/Code_Integer" |
2 imports Main "~~/src/HOL/Library/Code_Integer" |
3 uses |
|
4 "../../antiquote_setup.ML" |
|
5 "../../more_antiquote.ML" |
|
6 begin |
3 begin |
|
4 |
|
5 ML_file "../../antiquote_setup.ML" |
|
6 ML_file "../../more_antiquote.ML" |
7 |
7 |
8 setup {* |
8 setup {* |
9 Antiquote_Setup.setup #> |
9 Antiquote_Setup.setup #> |
10 More_Antiquote.setup #> |
10 More_Antiquote.setup #> |
11 Code_Target.set_default_code_width 74 |
11 Code_Target.set_default_code_width 74 |