equal
deleted
inserted
replaced
898 % |
898 % |
899 \isadelimmlref |
899 \isadelimmlref |
900 % |
900 % |
901 \endisadelimmlref |
901 \endisadelimmlref |
902 % |
902 % |
|
903 \isadelimmlantiq |
|
904 % |
|
905 \endisadelimmlantiq |
|
906 % |
|
907 \isatagmlantiq |
|
908 % |
|
909 \begin{isamarkuptext}% |
|
910 \begin{matharray}{rcl} |
|
911 \indexdef{}{ML antiquotation}{attributes}\hypertarget{ML antiquotation.attributes}{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
|
912 \end{matharray} |
|
913 |
|
914 \begin{railoutput} |
|
915 \rail@begin{1}{} |
|
916 \rail@term{\hyperlink{ML antiquotation.attributes}{\mbox{\isa{attributes}}}}[] |
|
917 \rail@nont{\isa{attributes}}[] |
|
918 \rail@end |
|
919 \end{railoutput} |
|
920 |
|
921 |
|
922 \begin{description} |
|
923 |
|
924 \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}attributes\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{7D}{\isacharbraceright}}} embeds attribute source |
|
925 representation into the ML text, which is particularly useful with |
|
926 declarations like \verb|Local_Theory.note|. Attribute names are |
|
927 internalized at compile time, but the source is unevaluated. This |
|
928 means attributes with formal arguments (types, terms, theorems) may |
|
929 be subject to odd effects of dynamic scoping! |
|
930 |
|
931 \end{description}% |
|
932 \end{isamarkuptext}% |
|
933 \isamarkuptrue% |
|
934 % |
|
935 \endisatagmlantiq |
|
936 {\isafoldmlantiq}% |
|
937 % |
|
938 \isadelimmlantiq |
|
939 % |
|
940 \endisadelimmlantiq |
|
941 % |
903 \isadelimmlex |
942 \isadelimmlex |
904 % |
943 % |
905 \endisadelimmlex |
944 \endisadelimmlex |
906 % |
945 % |
907 \isatagmlex |
946 \isatagmlex |