equal
deleted
inserted
replaced
561 text %mlantiq {* |
561 text %mlantiq {* |
562 \begin{matharray}{rcl} |
562 \begin{matharray}{rcl} |
563 @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\ |
563 @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\ |
564 \end{matharray} |
564 \end{matharray} |
565 |
565 |
566 @{rail " |
566 @{rail \<open> |
567 @@{ML_antiquotation attributes} attributes |
567 @@{ML_antiquotation attributes} attributes |
568 "} |
568 \<close>} |
569 |
569 |
570 \begin{description} |
570 \begin{description} |
571 |
571 |
572 \item @{text "@{attributes [\<dots>]}"} embeds attribute source |
572 \item @{text "@{attributes [\<dots>]}"} embeds attribute source |
573 representation into the ML text, which is particularly useful with |
573 representation into the ML text, which is particularly useful with |