618 @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ |
618 @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ |
619 @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\ |
619 @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\ |
620 @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ |
620 @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ |
621 @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ |
621 @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ |
622 |
622 |
623 @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\ |
623 @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\ |
624 \end{supertabular} |
624 \end{supertabular} |
625 \end{center} |
625 \end{center} |
626 |
626 |
627 The token categories @{syntax (inner) num_token}, @{syntax (inner) |
627 The token categories @{syntax (inner) num_token}, @{syntax (inner) |
628 float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner) |
628 float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner) |
629 xstr} are not used in Pure. Object-logics may implement numerals |
629 str_token} are not used in Pure. Object-logics may implement numerals |
630 and string constants by adding appropriate syntax declarations, |
630 and string constants by adding appropriate syntax declarations, |
631 together with some translation functions (e.g.\ see Isabelle/HOL). |
631 together with some translation functions (e.g.\ see Isabelle/HOL). |
632 |
632 |
633 The derived categories @{syntax_def (inner) num_const}, @{syntax_def |
633 The derived categories @{syntax_def (inner) num_const}, @{syntax_def |
634 (inner) float_const}, and @{syntax_def (inner) num_const} provide |
634 (inner) float_const}, and @{syntax_def (inner) num_const} provide |