equal
deleted
inserted
replaced
3 uses |
3 uses |
4 "../../antiquote_setup.ML" |
4 "../../antiquote_setup.ML" |
5 "../../more_antiquote.ML" |
5 "../../more_antiquote.ML" |
6 begin |
6 begin |
7 |
7 |
|
8 setup {* Antiquote_Setup.setup #> More_Antiquote.setup *} |
|
9 |
|
10 |
8 end |
11 end |