equal
deleted
inserted
replaced
797 translation functions may depend on the current theory or proof |
797 translation functions may depend on the current theory or proof |
798 context. This allows to implement advanced syntax mechanisms, as |
798 context. This allows to implement advanced syntax mechanisms, as |
799 translations functions may refer to specific theory declarations or |
799 translations functions may refer to specific theory declarations or |
800 auxiliary proof data. |
800 auxiliary proof data. |
801 |
801 |
802 See also \cite[\S8]{isabelle-ref} for more information on the |
802 See also \cite{isabelle-ref} for more information on the general |
803 general concept of syntax transformations in Isabelle. |
803 concept of syntax transformations in Isabelle. |
804 |
804 |
805 %FIXME proper antiquotations |
805 %FIXME proper antiquotations |
806 \begin{ttbox} |
806 \begin{ttbox} |
807 val parse_ast_translation: |
807 val parse_ast_translation: |
808 (string * (Proof.context -> ast list -> ast)) list |
808 (string * (Proof.context -> ast list -> ast)) list |