equal
deleted
inserted
replaced
2 imports |
2 imports |
3 Complex_Main |
3 Complex_Main |
4 "~~/src/HOL/Library/Dlist" |
4 "~~/src/HOL/Library/Dlist" |
5 "~~/src/HOL/Library/RBT" |
5 "~~/src/HOL/Library/RBT" |
6 "~~/src/HOL/Library/Mapping" |
6 "~~/src/HOL/Library/Mapping" |
7 uses |
|
8 "../../antiquote_setup.ML" |
|
9 "../../more_antiquote.ML" |
|
10 begin |
7 begin |
|
8 |
|
9 ML_file "../../antiquote_setup.ML" |
|
10 ML_file "../../more_antiquote.ML" |
11 |
11 |
12 setup {* |
12 setup {* |
13 Antiquote_Setup.setup #> |
13 Antiquote_Setup.setup #> |
14 More_Antiquote.setup #> |
14 More_Antiquote.setup #> |
15 let |
15 let |