779 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
779 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
780 not yet used to type the variables: this must be done by type-inference later |
780 not yet used to type the variables: this must be done by type-inference later |
781 on. Since types are part of the inner syntax they are strings with some |
781 on. Since types are part of the inner syntax they are strings with some |
782 encoded information (see previous section). If a mixfix-syntax is |
782 encoded information (see previous section). If a mixfix-syntax is |
783 present for a variable, then it is stored in the |
783 present for a variable, then it is stored in the |
784 @{ML Mixfix}\footnote{FIXME: access to Mixfix data structure} data structure; |
784 @{ML Mixfix} data structure; no syntax translation is indicated by @{ML_ind NoSyn in Syntax}. |
785 no syntax translation is indicated by @{ML_ind NoSyn}. |
|
786 |
785 |
787 \begin{readmore} |
786 \begin{readmore} |
788 The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
787 The data structure for mixfix annotations are implemented in |
|
788 @{ML_file "Pure/Syntax/mixfix.ML"} and @{ML_file "Pure/Syntax/syntax.ML"}. |
789 \end{readmore} |
789 \end{readmore} |
790 |
790 |
791 Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a |
791 Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a |
792 list of introduction rules, that is propositions with theorem annotations |
792 list of introduction rules, that is propositions with theorem annotations |
793 such as rule names and attributes. The introduction rules are propositions |
793 such as rule names and attributes. The introduction rules are propositions |