src/Doc/LaTeXsugar/Sugar.thy
changeset 49628 8262d35eff20
parent 49239 fdac10715b6b
child 53015 a1119cf551e8
--- a/src/Doc/LaTeXsugar/Sugar.thy	Fri Sep 28 08:09:28 2012 +0200
+++ b/src/Doc/LaTeXsugar/Sugar.thy	Fri Sep 28 08:39:48 2012 +0200
@@ -525,6 +525,16 @@
 \end{quote}
 The \texttt{isabelle} environment is the one defined in the standard file
 \texttt{isabelle.sty} which most likely you are loading anyway.
+
+
+\section{Antiquotation}
+
+You want to show a constant and its type? Instead of going
+\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
+you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
+\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
+\verb!@!\verb!{const_typ length}! produces @{const_typ length}.
+
 *}
 
 (*<*)