equal
deleted
inserted
replaced
802 %FIXME proper antiquotations |
802 %FIXME proper antiquotations |
803 \begin{ttbox} |
803 \begin{ttbox} |
804 val parse_ast_translation : (string * (ast list -> ast)) list |
804 val parse_ast_translation : (string * (ast list -> ast)) list |
805 val parse_translation : (string * (term list -> term)) list |
805 val parse_translation : (string * (term list -> term)) list |
806 val print_translation : (string * (term list -> term)) list |
806 val print_translation : (string * (term list -> term)) list |
807 val typed_print_translation : |
807 val typed_print_translation : (string * (typ -> term list -> term)) list |
808 (string * (bool -> typ -> term list -> term)) list |
|
809 val print_ast_translation : (string * (ast list -> ast)) list |
808 val print_ast_translation : (string * (ast list -> ast)) list |
810 \end{ttbox} |
809 \end{ttbox} |
811 |
810 |
812 If the @{text "(advanced)"} option is given, the corresponding |
811 If the @{text "(advanced)"} option is given, the corresponding |
813 translation functions may depend on the current theory or proof |
812 translation functions may depend on the current theory or proof |
825 val parse_translation: |
824 val parse_translation: |
826 (string * (Proof.context -> term list -> term)) list |
825 (string * (Proof.context -> term list -> term)) list |
827 val print_translation: |
826 val print_translation: |
828 (string * (Proof.context -> term list -> term)) list |
827 (string * (Proof.context -> term list -> term)) list |
829 val typed_print_translation: |
828 val typed_print_translation: |
830 (string * (Proof.context -> bool -> typ -> term list -> term)) list |
829 (string * (Proof.context -> typ -> term list -> term)) list |
831 val print_ast_translation: |
830 val print_ast_translation: |
832 (string * (Proof.context -> ast list -> ast)) list |
831 (string * (Proof.context -> ast list -> ast)) list |
833 \end{ttbox} |
832 \end{ttbox} |
834 *} |
833 *} |
835 |
834 |