equal
deleted
inserted
replaced
1 (* Title: Pure/Syntax/sextension.ML |
1 (* Title: Pure/Syntax/sextension.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 |
4 |
5 Syntax extensions (external interface): mixfix declarations, syntax rules, |
5 Syntax extensions (external interface): mixfix declarations, infixes, |
6 infixes, binders and the Pure syntax. |
6 binders, translation rules / functions and the Pure syntax. |
7 |
7 |
8 TODO: |
8 TODO: |
9 move ast_to_term (?) |
9 move ast_to_term (?) |
10 *) |
10 *) |
11 |
11 |