src/Doc/LaTeXsugar/Sugar.thy
changeset 49628 8262d35eff20
parent 49239 fdac10715b6b
child 53015 a1119cf551e8
equal deleted inserted replaced
49627:34ada66545ca 49628:8262d35eff20
   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 (*>*)