686 |
686 |
687 |
687 |
688 \section{Translation functions} \label{sec:tr_funs} |
688 \section{Translation functions} \label{sec:tr_funs} |
689 \index{translations|(} |
689 \index{translations|(} |
690 % |
690 % |
691 This section describes the translation function mechanism. By writing |
691 This section describes the translation function mechanism. By writing \ML{} |
692 \ML{} functions, you can do almost everything to terms or \AST{}s |
692 functions, you can do almost everything to terms or \AST{}s during parsing and |
693 during parsing and printing. The logic \LK\ is a good example of |
693 printing. The logic LK is a good example of sophisticated transformations |
694 sophisticated transformations between internal and external |
694 between internal and external representations of sequents; here, macros would |
695 representations of sequents; here, macros would be useless. |
695 be useless. |
696 |
696 |
697 A full understanding of translations requires some familiarity |
697 A full understanding of translations requires some familiarity |
698 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ}, |
698 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ}, |
699 {\tt Syntax.ast} and the encodings of types and terms as such at the various |
699 {\tt Syntax.ast} and the encodings of types and terms as such at the various |
700 stages of the parsing or printing process. Most users should never need to |
700 stages of the parsing or printing process. Most users should never need to |