equal
deleted
inserted
replaced
523 \texttt{\char`\\}\emph{snippetname}\\ |
523 \texttt{\char`\\}\emph{snippetname}\\ |
524 \verb!\end{isabelle}! |
524 \verb!\end{isabelle}! |
525 \end{quote} |
525 \end{quote} |
526 The \texttt{isabelle} environment is the one defined in the standard file |
526 The \texttt{isabelle} environment is the one defined in the standard file |
527 \texttt{isabelle.sty} which most likely you are loading anyway. |
527 \texttt{isabelle.sty} which most likely you are loading anyway. |
|
528 |
|
529 |
|
530 \section{Antiquotation} |
|
531 |
|
532 You want to show a constant and its type? Instead of going |
|
533 \verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!, |
|
534 you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation |
|
535 \texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example, |
|
536 \verb!@!\verb!{const_typ length}! produces @{const_typ length}. |
|
537 |
528 *} |
538 *} |
529 |
539 |
530 (*<*) |
540 (*<*) |
531 end |
541 end |
532 (*>*) |
542 (*>*) |