equal
deleted
inserted
replaced
1 theory Base |
1 theory Base |
2 imports Main LaTeXsugar |
2 imports Main |
|
3 "~~/src/HOL/Library/LaTeXsugar" |
3 uses |
4 uses |
4 ("output_tutorial.ML") |
5 ("output_tutorial.ML") |
5 ("antiquote_setup.ML") |
6 ("antiquote_setup.ML") |
6 begin |
7 begin |
7 |
8 |