equal
deleted
inserted
replaced
1 theory Base |
1 theory Base |
2 imports Main |
2 imports Main |
3 "~~/src/HOL/Library/LaTeXsugar" |
3 "~~/src/HOL/Library/LaTeXsugar" |
4 keywords "ML" "setup" "local_setup" :: thy_decl and |
4 (*keywords "ML" "setup" "local_setup" :: thy_decl and |
5 "ML_prf" :: prf_decl and |
5 "ML_prf" :: prf_decl and |
6 "ML_val" :: diag |
6 "ML_val" :: diag |
|
7 *) |
7 uses |
8 uses |
8 ("output_tutorial.ML") |
9 ("output_tutorial.ML") |
9 ("antiquote_setup.ML") |
10 ("antiquote_setup.ML") |
10 begin |
11 begin |
11 |
12 |