--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Sugar/Sugar.thy Sat Apr 05 11:37:00 2014 +0200
@@ -0,0 +1,542 @@
+(*<*)
+theory Sugar
+imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
+begin
+(*>*)
+text{*
+\section{Introduction}
+
+This document is for those Isabelle users who have mastered
+the art of mixing \LaTeX\ text and Isabelle theories and never want to
+typeset a theorem by hand anymore because they have experienced the
+bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
+and seeing Isabelle typeset it for them:
+@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
+No typos, no omissions, no sweat.
+If you have not experienced that joy, read Chapter 4, \emph{Presenting
+Theories}, \cite{LNCS2283} first.
+
+If you have mastered the art of Isabelle's \emph{antiquotations},
+i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
+you may be tempted to think that all readers of the stunning ps or pdf
+documents you can now produce at the drop of a hat will be struck with
+awe at the beauty unfolding in front of their eyes. Until one day you
+come across that very critical of readers known as the ``common referee''.
+He has the nasty habit of refusing to understand unfamiliar notation
+like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
+explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
+\<rbrakk>"} for anything other than denotational semantics is a cardinal sin
+that must be punished by instant rejection.
+
+
+This document shows you how to make Isabelle and \LaTeX\ cooperate to
+produce ordinary looking mathematics that hides the fact that it was
+typeset by a machine. You merely need to load the right files:
+\begin{itemize}
+\item Import theory \texttt{LaTeXsugar} in the header of your own
+theory. You may also want bits of \texttt{OptionalSugar}, which you can
+copy selectively into your own theory or import as a whole. Both
+theories live in \texttt{HOL/Library} and are found automatically.
+
+\item Should you need additional \LaTeX\ packages (the text will tell
+you so), you include them at the beginning of your \LaTeX\ document,
+typically in \texttt{root.tex}. For a start, you should
+\verb!\usepackage{amssymb}! --- otherwise typesetting
+@{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
+@{text"\<nexists>"} is missing.
+\end{itemize}
+
+
+\section{HOL syntax}
+
+\subsection{Logic}
+
+The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
+
+The predefined constructs @{text"if"}, @{text"let"} and
+@{text"case"} are set in sans serif font to distinguish them from
+other functions. This improves readability:
+\begin{itemize}
+\item @{term"if b then e\<^sub>1 else e\<^sub>2"} instead of @{text"if b then e\<^sub>1 else e\<^sub>2"}.
+\item @{term"let x = e\<^sub>1 in e\<^sub>2"} instead of @{text"let x = e\<^sub>1 in e\<^sub>2"}.
+\item @{term"case x of True \<Rightarrow> e\<^sub>1 | False \<Rightarrow> e\<^sub>2"} instead of\\
+ @{text"case x of True \<Rightarrow> e\<^sub>1 | False \<Rightarrow> e\<^sub>2"}.
+\end{itemize}
+
+\subsection{Sets}
+
+Although set syntax in HOL is already close to
+standard, we provide a few further improvements:
+\begin{itemize}
+\item @{term"{x. P}"} instead of @{text"{x. P}"}.
+\item @{term"{}"} instead of @{text"{}"}, where
+ @{term"{}"} is also input syntax.
+\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
+\end{itemize}
+
+
+\subsection{Lists}
+
+If lists are used heavily, the following notations increase readability:
+\begin{itemize}
+\item @{term"x # xs"} instead of @{text"x # xs"},
+ where @{term"x # xs"} is also input syntax.
+If you prefer more space around the $\cdot$ you have to redefine
+\verb!\isasymcdot! in \LaTeX:
+\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
+
+\item @{term"length xs"} instead of @{text"length xs"}.
+\item @{term"nth xs n"} instead of @{text"nth xs n"},
+ the $n$th element of @{text xs}.
+
+\item Human readers are good at converting automatically from lists to
+sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
+conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
+becomes @{prop"x \<in> set xs"}.
+
+\item The @{text"@"} operation associates implicitly to the right,
+which leads to unpleasant line breaks if the term is too long for one
+line. To avoid this, \texttt{OptionalSugar} contains syntax to group
+@{text"@"}-terms to the left before printing, which leads to better
+line breaking behaviour:
+@{term[display]"term\<^sub>0 @ term\<^sub>1 @ term\<^sub>2 @ term\<^sub>3 @ term\<^sub>4 @ term\<^sub>5 @ term\<^sub>6 @ term\<^sub>7 @ term\<^sub>8 @ term\<^sub>9 @ term\<^sub>1\<^sub>0"}
+
+\end{itemize}
+
+
+\subsection{Numbers}
+
+Coercions between numeric types are alien to mathematicians who
+consider, for example, @{typ nat} as a subset of @{typ int}.
+\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
+as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
+@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
+@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
+as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
+hidden.
+
+
+\section{Printing theorems}
+
+\subsection{Question marks}
+
+If you print anything, especially theorems, containing
+schematic variables they are prefixed with a question mark:
+\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
+you would rather not see the question marks. There is an attribute
+\verb!no_vars! that you can attach to the theorem that turns its
+schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
+results in @{thm conjI[no_vars]}.
+
+This \verb!no_vars! business can become a bit tedious.
+If you would rather never see question marks, simply put
+\begin{quote}
+\verb!options [show_question_marks = false]!
+\end{quote}
+into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
+The rest of this document is produced with this flag set to \texttt{false}.
+
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
+e.g. @{text"x1.0"}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^sub>1! and
+obtain the much nicer @{text"x\<^sub>1"}. *}
+
+(*<*)declare [[show_question_marks = false]](*>*)
+
+subsection {*Qualified names*}
+
+text{* If there are multiple declarations of the same name, Isabelle prints
+the qualified name, for example @{text "T.length"}, where @{text T} is the
+theory it is defined in, to distinguish it from the predefined @{const[source]
+"List.length"}. In case there is no danger of confusion, you can insist on
+short names (no qualifiers) by setting the \verb!names_short!
+configuration option in the context.
+
+
+\subsection {Variable names\label{sec:varnames}}
+
+It sometimes happens that you want to change the name of a
+variable in a theorem before printing it. This can easily be achieved
+with the help of Isabelle's instantiation attribute \texttt{where}:
+@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
+\begin{quote}
+\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
+\end{quote}
+To support the ``\_''-notation for irrelevant variables
+the constant \texttt{DUMMY} has been introduced:
+@{thm fst_conv[of _ DUMMY]} is produced by
+\begin{quote}
+\verb!@!\verb!{thm fst_conv[of _ DUMMY]}!
+\end{quote}
+Variables that are bound by quantifiers or lambdas cannot be renamed
+like this. Instead, the attribute \texttt{rename\_abs} does the
+job. It expects a list of names or underscores, similar to the
+\texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\end{quote}
+produces @{thm split_paired_All[rename_abs _ l r]}.
+
+
+\subsection{Inference rules}
+
+To print theorems as inference rules you need to include Didier
+R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
+for typesetting inference rules in your \LaTeX\ file.
+
+Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
+@{thm[mode=Rule] conjI}, even in the middle of a sentence.
+If you prefer your inference rule on a separate line, maybe with a name,
+\begin{center}
+@{thm[mode=Rule] conjI} {\sc conjI}
+\end{center}
+is produced by
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
+\verb!\end{center}!
+\end{quote}
+It is not recommended to use the standard \texttt{display} option
+together with \texttt{Rule} because centering does not work and because
+the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
+clash.
+
+Of course you can display multiple rules in this fashion:
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
+\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
+\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
+\verb!\end{center}!
+\end{quote}
+yields
+\begin{center}\small
+@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
+@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
+@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
+\end{center}
+
+The \texttt{mathpartir} package copes well if there are too many
+premises for one line:
+\begin{center}
+@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
+ G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
+\end{center}
+
+Limitations: 1. Premises and conclusion must each not be longer than
+the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again
+displayed with a horizontal line, which looks at least unusual.
+
+
+In case you print theorems without premises no rule will be printed by the
+\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
+\verb!\end{center}!
+\end{quote}
+yields
+\begin{center}
+@{thm[mode=Axiom] refl} {\sc refl}
+\end{center}
+
+
+\subsection{Displays and font sizes}
+
+When displaying theorems with the \texttt{display} option, for example as in
+\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
+set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
+which is also the style that regular theory text is set in, e.g. *}
+
+lemma "t = t"
+(*<*)oops(*>*)
+
+text{* \noindent Otherwise \verb!\isastyleminor! is used,
+which does not modify the font size (assuming you stick to the default
+\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
+normal font size throughout your text, include
+\begin{quote}
+\verb!\renewcommand{\isastyle}{\isastyleminor}!
+\end{quote}
+in \texttt{root.tex}. On the other hand, if you like the small font,
+just put \verb!\isastyle! in front of the text in question,
+e.g.\ at the start of one of the center-environments above.
+
+The advantage of the display option is that you can display a whole
+list of theorems in one go. For example,
+\verb!@!\verb!{thm[display] append.simps}!
+generates @{thm[display] append.simps}
+
+
+\subsection{If-then}
+
+If you prefer a fake ``natural language'' style you can produce
+the body of
+\newtheorem{theorem}{Theorem}
+\begin{theorem}
+@{thm[mode=IfThen] le_trans}
+\end{theorem}
+by typing
+\begin{quote}
+\verb!@!\verb!{thm[mode=IfThen] le_trans}!
+\end{quote}
+
+In order to prevent odd line breaks, the premises are put into boxes.
+At times this is too drastic:
+\begin{theorem}
+@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
+\end{theorem}
+In which case you should use \texttt{IfThenNoBox} instead of
+\texttt{IfThen}:
+\begin{theorem}
+@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
+\end{theorem}
+
+
+\subsection{Doing it yourself\label{sec:yourself}}
+
+If for some reason you want or need to present theorems your
+own way, you can extract the premises and the conclusion explicitly
+and combine them as you like:
+\begin{itemize}
+\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
+prints premise 1 of $thm$.
+\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
+prints the conclusion of $thm$.
+\end{itemize}
+For example, ``from @{thm (prem 2) conjI} and
+@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
+is produced by
+\begin{quote}
+\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
+\end{quote}
+Thus you can rearrange or hide premises and typeset the theorem as you like.
+Styles like \verb!(prem 1)! are a general mechanism explained
+in \S\ref{sec:styles}.
+
+
+\subsection{Patterns}
+
+
+In \S\ref{sec:varnames} we shows how to create patterns containing ``@{term DUMMY}''.
+You can drive this game even further and extend the syntax of let
+bindings such that certain functions like @{term fst}, @{term hd},
+etc.\ are printed as patterns. \texttt{OptionalSugar} provides the following:
+
+\begin{center}
+\begin{tabular}{l@ {~~produced by~~}l}
+@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
+@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
+@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
+@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
+@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
+\end{tabular}
+\end{center}
+
+
+\section {Styles\label{sec:styles}}
+
+The \verb!thm! antiquotation works nicely for single theorems, but
+sets of equations as used in definitions are more difficult to
+typeset nicely: people tend to prefer aligned @{text "="} signs.
+
+To deal with such cases where it is desirable to dive into the structure
+of terms and theorems, Isabelle offers antiquotations featuring ``styles'':
+
+\begin{quote}
+\verb!@!\verb!{thm (style) thm}!\\
+\verb!@!\verb!{prop (style) thm}!\\
+\verb!@!\verb!{term (style) term}!\\
+\verb!@!\verb!{term_type (style) term}!\\
+\verb!@!\verb!{typeof (style) term}!\\
+\end{quote}
+
+ A ``style'' is a transformation of a term. There are predefined
+ styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
+For example, the output
+\begin{center}
+\begin{tabular}{l@ {~~@{text "="}~~}l}
+@{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
+@{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
+\end{tabular}
+\end{center}
+is produced by the following code:
+\begin{quote}
+ \verb!\begin{center}!\\
+ \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
+ \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
+ \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
+ \verb!\end{tabular}!\\
+ \verb!\end{center}!
+\end{quote}
+Note the space between \verb!@! and \verb!{! in the tabular argument.
+It prevents Isabelle from interpreting \verb!@ {~~...~~}!
+as an antiquotation. The styles \verb!lhs! and \verb!rhs!
+extract the left hand side (or right hand side respectively) from the
+conclusion of propositions consisting of a binary operator
+(e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
+
+Likewise, \verb!concl! may be used as a style to show just the
+conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
+\begin{center}
+ @{thm hd_Cons_tl}
+\end{center}
+To print just the conclusion,
+\begin{center}
+ @{thm (concl) hd_Cons_tl}
+\end{center}
+type
+\begin{quote}
+ \verb!\begin{center}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
+ \verb!\end{center}!
+\end{quote}
+Beware that any options must be placed \emph{before} the style, as in this example.
+
+Further use cases can be found in \S\ref{sec:yourself}.
+If you are not afraid of ML, you may also define your own styles.
+Have a look at module @{ML_structure Term_Style}.
+
+
+\section {Proofs}
+
+Full proofs, even if written in beautiful Isar style, are
+likely to be too long and detailed to be included in conference
+papers, but some key lemmas might be of interest.
+It is usually easiest to put them in figures like the one in Fig.\
+\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
+*}
+text_raw {*
+ \begin{figure}
+ \begin{center}\begin{minipage}{0.6\textwidth}
+ \isastyleminor\isamarkuptrue
+*}
+lemma True
+proof -
+ -- "pretty trivial"
+ show True by force
+qed
+text_raw {*
+ \end{minipage}\end{center}
+ \caption{Example proof in a figure.}\label{fig:proof}
+ \end{figure}
+*}
+text {*
+
+\begin{quote}
+\small
+\verb!text_raw {!\verb!*!\\
+\verb! \begin{figure}!\\
+\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
+\verb! \isastyleminor\isamarkuptrue!\\
+\verb!*!\verb!}!\\
+\verb!lemma True!\\
+\verb!proof -!\\
+\verb! -- "pretty trivial"!\\
+\verb! show True by force!\\
+\verb!qed!\\
+\verb!text_raw {!\verb!*!\\
+\verb! \end{minipage}\end{center}!\\
+\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
+\verb! \end{figure}!\\
+\verb!*!\verb!}!
+\end{quote}
+
+Other theory text, e.g.\ definitions, can be put in figures, too.
+
+\section{Theory snippets}
+
+This section describes how to include snippets of a theory text in some other \LaTeX\ document.
+The typical scenario is that the description of your theory is not part of the theory text but
+a separate document that antiquotes bits of the theory. This works well for terms and theorems
+but there are no antiquotations, for example, for function definitions or proofs. Even if there are antiquotations,
+the output is usually a reformatted (by Isabelle) version of the input and may not look like
+you wanted it to look. Here is how to include a snippet of theory text (in \LaTeX\ form) in some
+other \LaTeX\ document, in 4 easy steps. Beware that these snippets are not processed by
+any antiquotation mechanism: the resulting \LaTeX\ text is more or less exactly what you wrote
+in the theory, without any added sugar.
+
+\subsection{Theory markup}
+
+Include some markers at the beginning and the end of the theory snippet you want to cut out.
+You have to place the following lines before and after the snippet, where snippets must always be
+consecutive lines of theory text:
+\begin{quote}
+\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
+\emph{theory text}\\
+\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
+\end{quote}
+where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
+and \texttt{2} are explained in a moment.
+
+\subsection{Generate the \texttt{.tex} file}
+
+Run your theory \texttt{T} with the \texttt{isabelle} \texttt{build} tool
+to generate the \LaTeX-file \texttt{T.tex} which is needed for the next step,
+extraction of marked snippets.
+You may also want to process \texttt{T.tex} to generate a pdf document.
+This requires a definition of \texttt{\char`\\snippet}:
+\begin{verbatim}
+\newcommand{\repeatisanl}[1]
+ {\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
+\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
+\end{verbatim}
+Parameter 2 and 3 of \texttt{\char`\\snippet} are numbers (the \texttt{1}
+and \texttt{2} above) and determine how many newlines are inserted before and after the snippet.
+Unfortunately \texttt{text\_raw} eats up all preceding and following newlines
+and they have to be inserted again in this manner. Otherwise the document generated from \texttt{T.tex}
+will look ugly around the snippets. It can take some iterations to get the number of required
+newlines exactly right.
+
+\subsection{Extract marked snippets}
+\label{subsec:extract}
+
+Extract the marked bits of text with a shell-level script, e.g.
+\begin{quote}
+\verb!sed -n '/\\snip{/,/endsnip/p' T.tex > !\emph{snippets}\verb!.tex!
+\end{quote}
+File \emph{snippets}\texttt{.tex} (the name is arbitrary) now contains a sequence of blocks like this
+\begin{quote}
+\verb!\snip{!\emph{snippetname}\verb!}{1}{2}{%!\\
+\emph{theory text}\\
+\verb!}%endsnip!
+\end{quote}
+
+\subsection{Including snippets}
+
+In the preamble of the document where the snippets are to be used you define \texttt{\char`\\snip}
+and input \emph{snippets}\texttt{.tex}:
+\begin{verbatim}
+\newcommand{\snip}[4]
+ {\expandafter\newcommand\csname #1\endcsname{#4}}
+\input{snippets}
+\end{verbatim}
+This definition of \texttt{\char`\\snip} simply has the effect of defining for each snippet
+\emph{snippetname} a \LaTeX\ command \texttt{\char`\\}\emph{snippetname}
+that produces the corresponding snippet text. In the body of your document you can display that text
+like this:
+\begin{quote}
+\verb!\begin{isabelle}!\\
+\texttt{\char`\\}\emph{snippetname}\\
+\verb!\end{isabelle}!
+\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}.
+
+*}
+
+(*<*)
+end
+(*>*)