src/Doc/LaTeXsugar/Sugar.thy
author blanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 50583 681edd111e9b
parent 49628 8262d35eff20
child 53015 a1119cf551e8
permissions -rw-r--r--
really honor pattern depth, and use 2 by default
     1 (*<*)
     2 theory Sugar
     3 imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
     4 begin
     5 (*>*)
     6 text{*
     7 \section{Introduction}
     8 
     9 This document is for those Isabelle users who have mastered
    10 the art of mixing \LaTeX\ text and Isabelle theories and never want to
    11 typeset a theorem by hand anymore because they have experienced the
    12 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
    13 and seeing Isabelle typeset it for them:
    14 @{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
    15 No typos, no omissions, no sweat.
    16 If you have not experienced that joy, read Chapter 4, \emph{Presenting
    17 Theories}, \cite{LNCS2283} first.
    18 
    19 If you have mastered the art of Isabelle's \emph{antiquotations},
    20 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
    21 you may be tempted to think that all readers of the stunning ps or pdf
    22 documents you can now produce at the drop of a hat will be struck with
    23 awe at the beauty unfolding in front of their eyes. Until one day you
    24 come across that very critical of readers known as the ``common referee''.
    25 He has the nasty habit of refusing to understand unfamiliar notation
    26 like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
    27 explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
    28 \<rbrakk>"} for anything other than denotational semantics is a cardinal sin
    29 that must be punished by instant rejection.
    30 
    31 
    32 This document shows you how to make Isabelle and \LaTeX\ cooperate to
    33 produce ordinary looking mathematics that hides the fact that it was
    34 typeset by a machine. You merely need to load the right files:
    35 \begin{itemize}
    36 \item Import theory \texttt{LaTeXsugar} in the header of your own
    37 theory.  You may also want bits of \texttt{OptionalSugar}, which you can
    38 copy selectively into your own theory or import as a whole.  Both
    39 theories live in \texttt{HOL/Library} and are found automatically.
    40 
    41 \item Should you need additional \LaTeX\ packages (the text will tell
    42 you so), you include them at the beginning of your \LaTeX\ document,
    43 typically in \texttt{root.tex}. For a start, you should
    44 \verb!\usepackage{amssymb}! --- otherwise typesetting
    45 @{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
    46 @{text"\<nexists>"} is missing.
    47 \end{itemize}
    48 
    49 
    50 \section{HOL syntax}
    51 
    52 \subsection{Logic}
    53 
    54 The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
    55 
    56 The predefined constructs @{text"if"}, @{text"let"} and
    57 @{text"case"} are set in sans serif font to distinguish them from
    58 other functions. This improves readability:
    59 \begin{itemize}
    60 \item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}.
    61 \item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
    62 \item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
    63       @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
    64 \end{itemize}
    65 
    66 \subsection{Sets}
    67 
    68 Although set syntax in HOL is already close to
    69 standard, we provide a few further improvements:
    70 \begin{itemize}
    71 \item @{term"{x. P}"} instead of @{text"{x. P}"}.
    72 \item @{term"{}"} instead of @{text"{}"}, where
    73  @{term"{}"} is also input syntax.
    74 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
    75 \end{itemize}
    76 
    77 
    78 \subsection{Lists}
    79 
    80 If lists are used heavily, the following notations increase readability:
    81 \begin{itemize}
    82 \item @{term"x # xs"} instead of @{text"x # xs"},
    83       where @{term"x # xs"} is also input syntax.
    84 If you prefer more space around the $\cdot$ you have to redefine
    85 \verb!\isasymcdot! in \LaTeX:
    86 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
    87 
    88 \item @{term"length xs"} instead of @{text"length xs"}.
    89 \item @{term"nth xs n"} instead of @{text"nth xs n"},
    90       the $n$th element of @{text xs}.
    91 
    92 \item Human readers are good at converting automatically from lists to
    93 sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
    94 conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
    95 becomes @{prop"x \<in> set xs"}.
    96 
    97 \item The @{text"@"} operation associates implicitly to the right,
    98 which leads to unpleasant line breaks if the term is too long for one
    99 line. To avoid this, \texttt{OptionalSugar} contains syntax to group
   100 @{text"@"}-terms to the left before printing, which leads to better
   101 line breaking behaviour:
   102 @{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
   103 
   104 \end{itemize}
   105 
   106 
   107 \subsection{Numbers}
   108 
   109 Coercions between numeric types are alien to mathematicians who
   110 consider, for example, @{typ nat} as a subset of @{typ int}.
   111 \texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
   112 as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
   113 @{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
   114 @{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
   115 as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
   116 hidden.
   117 
   118 
   119 \section{Printing theorems}
   120 
   121 \subsection{Question marks}
   122 
   123 If you print anything, especially theorems, containing
   124 schematic variables they are prefixed with a question mark:
   125 \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
   126 you would rather not see the question marks. There is an attribute
   127 \verb!no_vars! that you can attach to the theorem that turns its
   128 schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
   129 results in @{thm conjI[no_vars]}.
   130 
   131 This \verb!no_vars! business can become a bit tedious.
   132 If you would rather never see question marks, simply put
   133 \begin{quote}
   134 \verb!options [show_question_marks = false]!
   135 \end{quote}
   136 into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
   137 The rest of this document is produced with this flag set to \texttt{false}.
   138 
   139 Hint: Setting \verb!show_question_marks! to \texttt{false} only
   140 suppresses question marks; variables that end in digits,
   141 e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
   142 e.g. @{text"x1.0"}, their internal index. This can be avoided by
   143 turning the last digit into a subscript: write \verb!x\<^isub>1! and
   144 obtain the much nicer @{text"x\<^isub>1"}. *}
   145 
   146 (*<*)declare [[show_question_marks = false]](*>*)
   147 
   148 subsection {*Qualified names*}
   149 
   150 text{* If there are multiple declarations of the same name, Isabelle prints
   151 the qualified name, for example @{text "T.length"}, where @{text T} is the
   152 theory it is defined in, to distinguish it from the predefined @{const[source]
   153 "List.length"}. In case there is no danger of confusion, you can insist on
   154 short names (no qualifiers) by setting the \verb!names_short!
   155 configuration option in the context.
   156 
   157 
   158 \subsection {Variable names\label{sec:varnames}}
   159 
   160 It sometimes happens that you want to change the name of a
   161 variable in a theorem before printing it. This can easily be achieved
   162 with the help of Isabelle's instantiation attribute \texttt{where}:
   163 @{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
   164 \begin{quote}
   165 \verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
   166 \end{quote}
   167 To support the ``\_''-notation for irrelevant variables
   168 the constant \texttt{DUMMY} has been introduced:
   169 @{thm fst_conv[where b = DUMMY]} is produced by
   170 \begin{quote}
   171 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
   172 \end{quote}
   173 Variables that are bound by quantifiers or lambdas cannot be renamed
   174 like this. Instead, the attribute \texttt{rename\_abs} does the
   175 job. It expects a list of names or underscores, similar to the
   176 \texttt{of} attribute:
   177 \begin{quote}
   178 \verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
   179 \end{quote}
   180 produces @{thm split_paired_All[rename_abs _ l r]}.
   181 
   182 
   183 \subsection{Inference rules}
   184 
   185 To print theorems as inference rules you need to include Didier
   186 R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
   187 for typesetting inference rules in your \LaTeX\ file.
   188 
   189 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
   190 @{thm[mode=Rule] conjI}, even in the middle of a sentence.
   191 If you prefer your inference rule on a separate line, maybe with a name,
   192 \begin{center}
   193 @{thm[mode=Rule] conjI} {\sc conjI}
   194 \end{center}
   195 is produced by
   196 \begin{quote}
   197 \verb!\begin{center}!\\
   198 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
   199 \verb!\end{center}!
   200 \end{quote}
   201 It is not recommended to use the standard \texttt{display} option
   202 together with \texttt{Rule} because centering does not work and because
   203 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
   204 clash.
   205 
   206 Of course you can display multiple rules in this fashion:
   207 \begin{quote}
   208 \verb!\begin{center}!\\
   209 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
   210 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
   211 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
   212 \verb!\end{center}!
   213 \end{quote}
   214 yields
   215 \begin{center}\small
   216 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
   217 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
   218 @{thm[mode=Rule] disjI2} {\sc disjI$_2$}
   219 \end{center}
   220 
   221 The \texttt{mathpartir} package copes well if there are too many
   222 premises for one line:
   223 \begin{center}
   224 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
   225  G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
   226 \end{center}
   227 
   228 Limitations: 1. Premises and conclusion must each not be longer than
   229 the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
   230 displayed with a horizontal line, which looks at least unusual.
   231 
   232 
   233 In case you print theorems without premises no rule will be printed by the
   234 \texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
   235 \begin{quote}
   236 \verb!\begin{center}!\\
   237 \verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
   238 \verb!\end{center}!
   239 \end{quote}
   240 yields
   241 \begin{center}
   242 @{thm[mode=Axiom] refl} {\sc refl} 
   243 \end{center}
   244 
   245 
   246 \subsection{Displays and font sizes}
   247 
   248 When displaying theorems with the \texttt{display} option, for example as in
   249 \verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
   250 set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
   251 which is also the style that regular theory text is set in, e.g. *}
   252 
   253 lemma "t = t"
   254 (*<*)oops(*>*)
   255 
   256 text{* \noindent Otherwise \verb!\isastyleminor! is used,
   257 which does not modify the font size (assuming you stick to the default
   258 \verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
   259 normal font size throughout your text, include
   260 \begin{quote}
   261 \verb!\renewcommand{\isastyle}{\isastyleminor}!
   262 \end{quote}
   263 in \texttt{root.tex}. On the other hand, if you like the small font,
   264 just put \verb!\isastyle! in front of the text in question,
   265 e.g.\ at the start of one of the center-environments above.
   266 
   267 The advantage of the display option is that you can display a whole
   268 list of theorems in one go. For example,
   269 \verb!@!\verb!{thm[display] append.simps}!
   270 generates @{thm[display] append.simps}
   271 
   272 
   273 \subsection{If-then}
   274 
   275 If you prefer a fake ``natural language'' style you can produce
   276 the body of
   277 \newtheorem{theorem}{Theorem}
   278 \begin{theorem}
   279 @{thm[mode=IfThen] le_trans}
   280 \end{theorem}
   281 by typing
   282 \begin{quote}
   283 \verb!@!\verb!{thm[mode=IfThen] le_trans}!
   284 \end{quote}
   285 
   286 In order to prevent odd line breaks, the premises are put into boxes.
   287 At times this is too drastic:
   288 \begin{theorem}
   289 @{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   290 \end{theorem}
   291 In which case you should use \texttt{IfThenNoBox} instead of
   292 \texttt{IfThen}:
   293 \begin{theorem}
   294 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   295 \end{theorem}
   296 
   297 
   298 \subsection{Doing it yourself\label{sec:yourself}}
   299 
   300 If for some reason you want or need to present theorems your
   301 own way, you can extract the premises and the conclusion explicitly
   302 and combine them as you like:
   303 \begin{itemize}
   304 \item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
   305 prints premise 1 of $thm$.
   306 \item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
   307 prints the conclusion of $thm$.
   308 \end{itemize}
   309 For example, ``from @{thm (prem 2) conjI} and
   310 @{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
   311 is produced by
   312 \begin{quote}
   313 \verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
   314 \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
   315 \end{quote}
   316 Thus you can rearrange or hide premises and typeset the theorem as you like.
   317 Styles like \verb!(prem 1)! are a general mechanism explained
   318 in \S\ref{sec:styles}.
   319 
   320 
   321 \subsection{Patterns}
   322 
   323 
   324 In \S\ref{sec:varnames} we shows how to create patterns containing ``@{term DUMMY}''.
   325 You can drive this game even further and extend the syntax of let
   326 bindings such that certain functions like @{term fst}, @{term hd}, 
   327 etc.\ are printed as patterns. \texttt{OptionalSugar} provides the following:
   328 
   329 \begin{center}
   330 \begin{tabular}{l@ {~~produced by~~}l}
   331 @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
   332 @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
   333 @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
   334 @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
   335 @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
   336 \end{tabular}
   337 \end{center}
   338 
   339 
   340 \section {Styles\label{sec:styles}}
   341 
   342 The \verb!thm! antiquotation works nicely for single theorems, but
   343 sets of equations as used in definitions are more difficult to
   344 typeset nicely: people tend to prefer aligned @{text "="} signs.
   345 
   346 To deal with such cases where it is desirable to dive into the structure
   347 of terms and theorems, Isabelle offers antiquotations featuring ``styles'':
   348 
   349 \begin{quote}
   350 \verb!@!\verb!{thm (style) thm}!\\
   351 \verb!@!\verb!{prop (style) thm}!\\
   352 \verb!@!\verb!{term (style) term}!\\
   353 \verb!@!\verb!{term_type (style) term}!\\
   354 \verb!@!\verb!{typeof (style) term}!\\
   355 \end{quote}
   356 
   357  A ``style'' is a transformation of a term. There are predefined
   358  styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
   359 For example, the output
   360 \begin{center}
   361 \begin{tabular}{l@ {~~@{text "="}~~}l}
   362 @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
   363 @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
   364 \end{tabular}
   365 \end{center}
   366 is produced by the following code:
   367 \begin{quote}
   368   \verb!\begin{center}!\\
   369   \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
   370   \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
   371   \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
   372   \verb!\end{tabular}!\\
   373   \verb!\end{center}!
   374 \end{quote}
   375 Note the space between \verb!@! and \verb!{! in the tabular argument.
   376 It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   377 as an antiquotation. The styles \verb!lhs! and \verb!rhs!
   378 extract the left hand side (or right hand side respectively) from the
   379 conclusion of propositions consisting of a binary operator
   380 (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
   381 
   382 Likewise, \verb!concl! may be used as a style to show just the
   383 conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   384 \begin{center}
   385   @{thm hd_Cons_tl}
   386 \end{center}
   387 To print just the conclusion,
   388 \begin{center}
   389   @{thm (concl) hd_Cons_tl}
   390 \end{center}
   391 type
   392 \begin{quote}
   393   \verb!\begin{center}!\\
   394   \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
   395   \verb!\end{center}!
   396 \end{quote}
   397 Beware that any options must be placed \emph{before} the style, as in this example.
   398 
   399 Further use cases can be found in \S\ref{sec:yourself}.
   400 If you are not afraid of ML, you may also define your own styles.
   401 Have a look at module @{ML_struct Term_Style}.
   402 
   403 
   404 \section {Proofs}
   405 
   406 Full proofs, even if written in beautiful Isar style, are
   407 likely to be too long and detailed to be included in conference
   408 papers, but some key lemmas might be of interest.
   409 It is usually easiest to put them in figures like the one in Fig.\
   410 \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
   411 *}
   412 text_raw {*
   413   \begin{figure}
   414   \begin{center}\begin{minipage}{0.6\textwidth}  
   415   \isastyleminor\isamarkuptrue
   416 *}
   417 lemma True
   418 proof -
   419   -- "pretty trivial"
   420   show True by force
   421 qed
   422 text_raw {*    
   423   \end{minipage}\end{center}
   424   \caption{Example proof in a figure.}\label{fig:proof}
   425   \end{figure}
   426 *}
   427 text {*
   428 
   429 \begin{quote}
   430 \small
   431 \verb!text_raw {!\verb!*!\\
   432 \verb!  \begin{figure}!\\
   433 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
   434 \verb!  \isastyleminor\isamarkuptrue!\\
   435 \verb!*!\verb!}!\\
   436 \verb!lemma True!\\
   437 \verb!proof -!\\
   438 \verb!  -- "pretty trivial"!\\
   439 \verb!  show True by force!\\
   440 \verb!qed!\\
   441 \verb!text_raw {!\verb!*!\\
   442 \verb!  \end{minipage}\end{center}!\\
   443 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
   444 \verb!  \end{figure}!\\
   445 \verb!*!\verb!}!
   446 \end{quote}
   447 
   448 Other theory text, e.g.\ definitions, can be put in figures, too.
   449 
   450 \section{Theory snippets}
   451 
   452 This section describes how to include snippets of a theory text in some other \LaTeX\ document.
   453 The typical scenario is that the description of your theory is not part of the theory text but
   454 a separate document that antiquotes bits of the theory. This works well for terms and theorems
   455 but there are no antiquotations, for example, for function definitions or proofs. Even if there are antiquotations,
   456 the output is usually a reformatted (by Isabelle) version of the input and may not look like
   457 you wanted it to look. Here is how to include a snippet of theory text (in \LaTeX\ form) in some
   458 other \LaTeX\ document, in 4 easy steps. Beware that these snippets are not processed by
   459 any antiquotation mechanism: the resulting \LaTeX\ text is more or less exactly what you wrote
   460 in the theory, without any added sugar.
   461 
   462 \subsection{Theory markup}
   463 
   464 Include some markers at the beginning and the end of the theory snippet you want to cut out.
   465 You have to place the following lines before and after the snippet, where snippets must always be
   466 consecutive lines of theory text:
   467 \begin{quote}
   468 \verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
   469 \emph{theory text}\\
   470 \verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
   471 \end{quote}
   472 where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
   473 and \texttt{2} are explained in a moment.
   474 
   475 \subsection{Generate the \texttt{.tex} file}
   476 
   477 Run your theory \texttt{T} with the \texttt{isabelle} \texttt{build} tool
   478 to generate the \LaTeX-file \texttt{T.tex} which is needed for the next step,
   479 extraction of marked snippets.
   480 You may also want to process \texttt{T.tex} to generate a pdf document.
   481 This requires a definition of \texttt{\char`\\snippet}:
   482 \begin{verbatim}
   483 \newcommand{\repeatisanl}[1]
   484   {\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
   485 \newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
   486 \end{verbatim}
   487 Parameter 2 and 3 of \texttt{\char`\\snippet} are numbers (the \texttt{1}
   488 and \texttt{2} above) and determine how many newlines are inserted before and after the snippet.
   489 Unfortunately \texttt{text\_raw} eats up all preceding and following newlines
   490 and they have to be inserted again in this manner. Otherwise the document generated from \texttt{T.tex}
   491 will look ugly around the snippets. It can take some iterations to get the number of required
   492 newlines exactly right.
   493 
   494 \subsection{Extract marked snippets}
   495 \label{subsec:extract}
   496 
   497 Extract the marked bits of text with a shell-level script, e.g.
   498 \begin{quote}
   499 \verb!sed -n '/\\snip{/,/endsnip/p' T.tex > !\emph{snippets}\verb!.tex!
   500 \end{quote}
   501 File \emph{snippets}\texttt{.tex} (the name is arbitrary) now contains a sequence of blocks like this
   502 \begin{quote}
   503 \verb!\snip{!\emph{snippetname}\verb!}{1}{2}{%!\\
   504 \emph{theory text}\\
   505 \verb!}%endsnip!
   506 \end{quote}
   507 
   508 \subsection{Including snippets}
   509 
   510 In the preamble of the document where the snippets are to be used you define \texttt{\char`\\snip}
   511 and input \emph{snippets}\texttt{.tex}:
   512 \begin{verbatim}
   513 \newcommand{\snip}[4]
   514   {\expandafter\newcommand\csname #1\endcsname{#4}}
   515 \input{snippets}
   516 \end{verbatim}
   517 This definition of \texttt{\char`\\snip} simply has the effect of defining for each snippet
   518 \emph{snippetname} a \LaTeX\ command \texttt{\char`\\}\emph{snippetname}
   519 that produces the corresponding snippet text. In the body of your document you can display that text
   520 like this:
   521 \begin{quote}
   522 \verb!\begin{isabelle}!\\
   523 \texttt{\char`\\}\emph{snippetname}\\
   524 \verb!\end{isabelle}!
   525 \end{quote}
   526 The \texttt{isabelle} environment is the one defined in the standard file
   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 
   538 *}
   539 
   540 (*<*)
   541 end
   542 (*>*)