doc-src/LaTeXsugar/Sugar/Sugar.thy
author wenzelm
Tue May 17 18:10:36 2005 +0200 (2005-05-17)
changeset 15983 a53abeedc879
parent 15960 9bd6550dc004
child 16040 6e7616eba0b8
permissions -rw-r--r--
renamed show_var_qmarks to show_question_marks;
nipkow@15337
     1
(*<*)
nipkow@15337
     2
theory Sugar
kleing@15366
     3
imports LaTeXsugar OptionalSugar
nipkow@15337
     4
begin
nipkow@15337
     5
(*>*)
nipkow@15337
     6
nipkow@15337
     7
section "Introduction"
nipkow@15337
     8
kleing@15385
     9
text{* This document is for those Isabelle users who have mastered
nipkow@15337
    10
the art of mixing \LaTeX\ text and Isabelle theories and never want to
nipkow@15337
    11
typeset a theorem by hand anymore because they have experienced the
nipkow@15337
    12
bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
nipkow@15337
    13
and seeing Isabelle typeset it for them:
nipkow@15337
    14
@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
nipkow@15342
    15
No typos, no omissions, no sweat.
nipkow@15342
    16
If you have not experienced that joy, read Chapter 4, \emph{Presenting
nipkow@15342
    17
Theories}, \cite{LNCS2283} first.
nipkow@15337
    18
nipkow@15337
    19
If you have mastered the art of Isabelle's \emph{antiquotations},
nipkow@15337
    20
i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
nipkow@15337
    21
you may be tempted to think that all readers of the stunning ps or pdf
nipkow@15337
    22
documents you can now produce at the drop of a hat will be struck with
nipkow@15337
    23
awe at the beauty unfolding in front of their eyes. Until one day you
nipkow@15337
    24
come across that very critical of readers known as the ``common referee''.
nipkow@15337
    25
He has the nasty habit of refusing to understand unfamiliar notation
nipkow@15337
    26
like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
nipkow@15337
    27
explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
nipkow@15337
    28
\<rbrakk>"} for anything other than denotational semantics is a cardinal sin
nipkow@15342
    29
that must be punished by instant rejection.
nipkow@15337
    30
nipkow@15337
    31
nipkow@15337
    32
This document shows you how to make Isabelle and \LaTeX\ cooperate to
nipkow@15337
    33
produce ordinary looking mathematics that hides the fact that it was
nipkow@15471
    34
typeset by a machine. You merely need to load the right files:
nipkow@15471
    35
\begin{itemize}
nipkow@15471
    36
\item Import theory \texttt{LaTeXsugar} in the header of your own
nipkow@15471
    37
theory.  You may also want bits of \texttt{OptionalSugar}, which you can
nipkow@15471
    38
copy selectively into your own theory or import as a whole.  Both
nipkow@15471
    39
theories live in \texttt{HOL/Library} and are found automatically.
kleing@15378
    40
nipkow@15471
    41
\item Should you need additional \LaTeX\ packages (the text will tell
nipkow@15471
    42
you so), you include them at the beginning of your \LaTeX\ document,
nipkow@15471
    43
typically in \texttt{root.tex}.
nipkow@15471
    44
\end{itemize}
nipkow@15342
    45
*}
nipkow@15342
    46
nipkow@15342
    47
section{* HOL syntax*}
nipkow@15342
    48
nipkow@15342
    49
subsection{* Logic *}
nipkow@15342
    50
nipkow@15342
    51
text{* The predefined constructs @{text"if"}, @{text"let"} and
nipkow@15342
    52
@{text"case"} are set in sans serif font to distinguish them from
nipkow@15342
    53
other functions. This improves readability:
nipkow@15342
    54
\begin{itemize}
nipkow@15342
    55
\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"}.
nipkow@15342
    56
\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
nipkow@15342
    57
\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
nipkow@15342
    58
      @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
nipkow@15342
    59
\end{itemize}
nipkow@15342
    60
*}
nipkow@15342
    61
nipkow@15342
    62
subsection{* Sets *}
nipkow@15337
    63
nipkow@15342
    64
text{* Although set syntax in HOL is already close to
nipkow@15342
    65
standard, we provide a few further improvements:
nipkow@15342
    66
\begin{itemize}
nipkow@15342
    67
\item @{term"{x. P}"} instead of @{text"{x. P}"}.
nipkow@15342
    68
\item @{term"{}"} instead of @{text"{}"}.
nipkow@15342
    69
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
nipkow@15342
    70
\end{itemize}
nipkow@15342
    71
*}
nipkow@15342
    72
nipkow@15342
    73
subsection{* Lists *}
nipkow@15342
    74
nipkow@15342
    75
text{* If lists are used heavily, the following notations increase readability:
nipkow@15342
    76
\begin{itemize}
nipkow@15342
    77
\item @{term"x # xs"} instead of @{text"x # xs"}.
nipkow@15342
    78
      Exceptionally, @{term"x # xs"} is also input syntax.
nipkow@15342
    79
If you prefer more space around the $\cdot$ you have to redefine
nipkow@15342
    80
\verb!\isasymcdot! in \LaTeX:
nipkow@15342
    81
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
nipkow@15342
    82
nipkow@15342
    83
\item @{term"length xs"} instead of @{text"length xs"}.
kleing@15385
    84
\item @{term"nth xs n"} instead of @{text"nth xs n"},
nipkow@15342
    85
      the $n$th element of @{text xs}.
nipkow@15342
    86
kleing@15366
    87
\item The @{text"@"} operation associates implicitly to the right,
kleing@15366
    88
which leads to unpleasant line breaks if the term is too long for one
kleing@15366
    89
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
kleing@15366
    90
@{text"@"}-terms to the left before printing, which leads to better
kleing@15366
    91
line breaking behaviour:
wenzelm@15673
    92
@{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"}
kleing@15366
    93
nipkow@15342
    94
\end{itemize}
nipkow@15337
    95
*}
nipkow@15337
    96
nipkow@15337
    97
section "Printing theorems"
nipkow@15337
    98
nipkow@15689
    99
subsection "Question marks"
nipkow@15689
   100
nipkow@15689
   101
text{* If you print anything, especially theorems, containing
nipkow@15689
   102
schematic variables they are prefixed with a question mark:
nipkow@15689
   103
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
nipkow@15689
   104
you would rather not see the question marks. There is an attribute
nipkow@15689
   105
\verb!no_vars! that you can attach to the theorem that turns its
nipkow@15689
   106
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
nipkow@15689
   107
results in @{thm conjI[no_vars]}.
nipkow@15689
   108
nipkow@15689
   109
This \verb!no_vars! business can become a bit tedious.
nipkow@15689
   110
If you would rather never see question marks, simply put
nipkow@15689
   111
\begin{verbatim}
wenzelm@15983
   112
reset show_question_marks;
nipkow@15689
   113
\end{verbatim}
nipkow@15689
   114
at the beginning of your file \texttt{ROOT.ML}.
nipkow@15689
   115
The rest of this document is produced with this flag reset.
nipkow@15689
   116
*}
nipkow@15689
   117
wenzelm@15983
   118
(*<*)ML"reset show_question_marks"(*>*)
nipkow@15689
   119
nipkow@15337
   120
subsection "Inference rules"
nipkow@15337
   121
nipkow@15342
   122
text{* To print theorems as inference rules you need to include Didier
nipkow@15342
   123
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
nipkow@15342
   124
for typesetting inference rules in your \LaTeX\ file.
nipkow@15337
   125
nipkow@15689
   126
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
nipkow@15689
   127
@{thm[mode=Rule] conjI}, even in the middle of a sentence.
nipkow@15342
   128
If you prefer your inference rule on a separate line, maybe with a name,
nipkow@15342
   129
\begin{center}
nipkow@15689
   130
@{thm[mode=Rule] conjI} {\sc conjI}
nipkow@15342
   131
\end{center}
nipkow@15342
   132
is produced by
nipkow@15337
   133
\begin{quote}
nipkow@15337
   134
\verb!\begin{center}!\\
nipkow@15689
   135
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
nipkow@15337
   136
\verb!\end{center}!
nipkow@15337
   137
\end{quote}
nipkow@15342
   138
It is not recommended to use the standard \texttt{display} attribute
nipkow@15342
   139
together with \texttt{Rule} because centering does not work and because
nipkow@15342
   140
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
nipkow@15342
   141
clash.
nipkow@15342
   142
nipkow@15337
   143
Of course you can display multiple rules in this fashion:
nipkow@15337
   144
\begin{quote}
nipkow@15337
   145
\verb!\begin{center}\isastyle!\\
nipkow@15689
   146
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
nipkow@15689
   147
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
nipkow@15689
   148
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
nipkow@15337
   149
\verb!\end{center}!
nipkow@15337
   150
\end{quote}
nipkow@15337
   151
yields
nipkow@15337
   152
\begin{center}\isastyle
nipkow@15689
   153
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
nipkow@15689
   154
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
nipkow@15689
   155
@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
nipkow@15337
   156
\end{center}
nipkow@15337
   157
Note that we included \verb!\isastyle! to obtain
nipkow@15337
   158
the smaller font that otherwise comes only with \texttt{display}.
nipkow@15337
   159
nipkow@15342
   160
The \texttt{mathpartir} package copes well if there are too many
nipkow@15342
   161
premises for one line:
nipkow@15342
   162
\begin{center}
nipkow@15342
   163
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
nipkow@15342
   164
 G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
nipkow@15342
   165
\end{center}
nipkow@15342
   166
nipkow@15471
   167
Limitations: 1. Premises and conclusion must each not be longer than
nipkow@15471
   168
the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
nipkow@15471
   169
displayed with a horizontal line, which looks at least unusual.
nipkow@15471
   170
nipkow@15337
   171
*}
nipkow@15342
   172
nipkow@15342
   173
subsection{*If-then*}
nipkow@15342
   174
nipkow@15342
   175
text{* If you prefer a fake ``natural language'' style you can produce
nipkow@15342
   176
the body of
nipkow@15342
   177
\newtheorem{theorem}{Theorem}
nipkow@15342
   178
\begin{theorem}
nipkow@15689
   179
@{thm[mode=IfThen] le_trans}
nipkow@15342
   180
\end{theorem}
nipkow@15342
   181
by typing
nipkow@15342
   182
\begin{quote}
nipkow@15689
   183
\verb!@!\verb!{thm[mode=IfThen] le_trans}!
nipkow@15342
   184
\end{quote}
nipkow@15342
   185
nipkow@15342
   186
In order to prevent odd line breaks, the premises are put into boxes.
nipkow@15342
   187
At times this is too drastic:
nipkow@15342
   188
\begin{theorem}
nipkow@15342
   189
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
nipkow@15342
   190
\end{theorem}
nipkow@15342
   191
In which case you should use \texttt{mode=IfThenNoBox} instead of
nipkow@15342
   192
\texttt{mode=IfThen}:
nipkow@15342
   193
\begin{theorem}
nipkow@15342
   194
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
nipkow@15342
   195
\end{theorem}
kleing@15366
   196
*}
nipkow@15342
   197
kleing@15366
   198
subsection "Patterns"
kleing@15366
   199
kleing@15366
   200
text {*
kleing@15366
   201
  Sometimes functions ignore one or more of their
kleing@15366
   202
  arguments and some functional languages have nice 
nipkow@15689
   203
  syntax for that as in @{thm hd.simps [where xs=DUMMY]}.
kleing@15366
   204
kleing@15366
   205
  You can simulate this in Isabelle by instantiating the @{term xs} in
nipkow@15689
   206
  definition \mbox{@{thm hd.simps}} with a constant @{text DUMMY} that
kleing@15366
   207
  is printed as @{term DUMMY}. The code for the pattern above is 
nipkow@15689
   208
  \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
kleing@15366
   209
kleing@15366
   210
  You can drive this game even further and extend the syntax of let
kleing@15366
   211
  bindings such that certain functions like @{term fst}, @{term hd}, 
kleing@15368
   212
  etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
kleing@15368
   213
  following:
kleing@15366
   214
  
kleing@15366
   215
  \begin{center}
kleing@15366
   216
  \begin{tabular}{l@ {~~produced by~~}l}
kleing@15366
   217
  @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
kleing@15366
   218
  @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
kleing@15366
   219
  @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
kleing@15366
   220
  @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
kleing@15366
   221
  @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
kleing@15366
   222
  \end{tabular}
kleing@15366
   223
  \end{center}
kleing@15366
   224
*}
kleing@15366
   225
kleing@15366
   226
subsection "Proofs"
kleing@15366
   227
kleing@15366
   228
text {*
kleing@15367
   229
  Full proofs, even if written in beautiful Isar style, are likely to
kleing@15366
   230
  be too long and detailed to be included in conference papers, but
kleing@15366
   231
  some key lemmas might be of interest.
kleing@15366
   232
kleing@15366
   233
  It is usually easiest to put them in figures like the one in Fig.\
kleing@15366
   234
  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
kleing@15366
   235
  command:
kleing@15366
   236
*}
kleing@15366
   237
text_raw {*
kleing@15366
   238
  \begin{figure}
kleing@15366
   239
  \begin{center}\begin{minipage}{0.6\textwidth}  
kleing@15428
   240
  \isastyle\isamarkuptrue
kleing@15366
   241
*}
kleing@15366
   242
lemma True
kleing@15366
   243
proof -
kleing@15366
   244
  -- "pretty trivial"
kleing@15366
   245
  show True by force
kleing@15366
   246
qed
kleing@15428
   247
text_raw {*    
kleing@15366
   248
  \end{minipage}\end{center}
kleing@15366
   249
  \caption{Example proof in a figure.}\label{fig:proof}
kleing@15366
   250
  \end{figure}
kleing@15366
   251
*}
kleing@15366
   252
text {*
kleing@15366
   253
kleing@15366
   254
\begin{quote}
kleing@15366
   255
\small
kleing@15366
   256
\verb!text_raw {!\verb!*!\\
kleing@15366
   257
\verb!  \begin{figure}!\\
kleing@15366
   258
\verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
kleing@15428
   259
\verb!  \isastyle\isamarkuptrue!\\
kleing@15366
   260
\verb!*!\verb!}!\\
kleing@15366
   261
\verb!lemma True!\\
kleing@15366
   262
\verb!proof -!\\
kleing@15366
   263
\verb!  -- "pretty trivial"!\\
kleing@15366
   264
\verb!  show True by force!\\
kleing@15366
   265
\verb!qed!\\
kleing@15366
   266
\verb!text_raw {!\verb!*!\\
kleing@15366
   267
\verb!  \end{minipage}\end{center}!\\
kleing@15366
   268
\verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
kleing@15366
   269
\verb!  \end{figure}!\\
kleing@15366
   270
\verb!*!\verb!}!
kleing@15366
   271
\end{quote}
kleing@15366
   272
  
nipkow@15342
   273
*}
nipkow@15342
   274
haftmann@15917
   275
subsection "Styles"
haftmann@15917
   276
haftmann@15917
   277
text {*
nipkow@15953
   278
  The \verb!thm! antiquotation works nicely for single theorems, but
haftmann@15917
   279
  sets of equations as used in definitions are more difficult to
haftmann@15917
   280
  typeset nicely: for some reason people tend to prefer aligned 
haftmann@15917
   281
  @{text "="} signs.
haftmann@15917
   282
haftmann@15917
   283
  To deal with such cases where it is desirable to dive into the structure
haftmann@15917
   284
  of terms and theorems, Isabelle offers two antiquotations featuring
haftmann@15917
   285
  ``styles'':
haftmann@15917
   286
haftmann@15917
   287
    \begin{quote}
haftmann@15917
   288
    \verb!@!\verb!{thm_style stylename thm}!\\
haftmann@15917
   289
    \verb!@!\verb!{term_style stylename term}!
haftmann@15917
   290
    \end{quote}
haftmann@15917
   291
nipkow@15953
   292
  A ``style'' is a transformation of terms. There are three predefined
nipkow@15953
   293
  styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious
nipkow@15953
   294
  meanings. For example, the output
haftmann@15917
   295
  \begin{center}
haftmann@15917
   296
  \begin{tabular}{l@ {~~@{text "="}~~}l}
haftmann@15917
   297
  @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
haftmann@15917
   298
  @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
haftmann@15917
   299
  \end{tabular}
haftmann@15917
   300
  \end{center}
haftmann@15917
   301
  is produced by the following code:
haftmann@15917
   302
  \begin{quote}
haftmann@15917
   303
    \verb!\begin{center}!\\
haftmann@15917
   304
    \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
haftmann@15917
   305
    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
haftmann@15917
   306
    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
haftmann@15917
   307
    \verb!\end{tabular}!\\
haftmann@15917
   308
    \verb!\end{center}!
haftmann@15917
   309
  \end{quote}
haftmann@15917
   310
  Note the space between \verb!@! and \verb!{! in the tabular argument.
haftmann@15917
   311
  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
nipkow@15953
   312
  as an antiquotation. Both styles \verb!lhs! and \verb!rhs! 
haftmann@15917
   313
  try to be smart about the interpretation of the theorem they transform
haftmann@15917
   314
  they work just as well for meta equality @{text "\<equiv>"} and other
haftmann@15917
   315
  binary operators like @{text "<"}.
haftmann@15917
   316
haftmann@15917
   317
  Likewise \verb!conclusion! may be used as style to show just the conclusion
haftmann@15917
   318
  of a formula:
haftmann@15917
   319
  \begin{center}
haftmann@15917
   320
    @{thm_style conclusion hd_Cons_tl}
haftmann@15917
   321
  \end{center}
haftmann@15917
   322
  is produced by
haftmann@15917
   323
  \begin{quote}
haftmann@15917
   324
    \verb!\begin{center}!\\
haftmann@15917
   325
    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
haftmann@15917
   326
    \verb!\end{center}!
haftmann@15917
   327
  \end{quote}
haftmann@15917
   328
nipkow@15953
   329
  If you are not afraid of ML, you may also define your own styles.
haftmann@15960
   330
  A style is implemented by an ML function of type
haftmann@15960
   331
  \verb!Proof.context -> term -> term!.
haftmann@15960
   332
  Have a look at the following example:
haftmann@15960
   333
haftmann@15917
   334
  \begin{quote}
haftmann@15917
   335
    \verb!setup {!\verb!*!\\
haftmann@15917
   336
    \verb!let!\\
haftmann@15960
   337
    \verb!  fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\
haftmann@15960
   338
    \verb!    | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\
haftmann@15960
   339
    \verb!    | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\
haftmann@15960
   340
    \verb!    | my_lhs ctxt (_ $ t $ _) = t!\\
haftmann@15960
   341
    \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
wenzelm@15983
   342
    \verb!  in [TermStyle.add_style "new_lhs" my_lhs]!\\
haftmann@15917
   343
    \verb!end;!\\
haftmann@15917
   344
    \verb!*!\verb!}!\\
haftmann@15917
   345
  \end{quote}
haftmann@15960
   346
haftmann@15960
   347
  This example indeed shows a way the \verb!lhs! style could be implemented;
haftmann@15960
   348
  note that the real implementation is more sophisticated.
haftmann@15960
   349
nipkow@15953
   350
  This code must go into your theory file, not as part of your
nipkow@15953
   351
  \LaTeX\ text but as a separate command in front of it.
haftmann@15917
   352
  Like in this example, it is recommended to put the definition of the style
haftmann@15917
   353
  function into a \verb!let! expression, in order not to pollute the
haftmann@15960
   354
  ML global namespace. Each style receives the current proof context
haftmann@15960
   355
  as first argument; this is necessary in situations where the current proof
haftmann@15960
   356
  context has an impact on the style (which is the case e.~g.~when the
haftmann@15960
   357
  style has some object-logic specific behaviour).
haftmann@15960
   358
haftmann@15960
   359
  The mapping from identifier name to the style function
haftmann@15960
   360
  is done by the \verb!Style.update_style! expression which expects the desired
haftmann@15960
   361
  style name and the style function as arguments.
haftmann@15960
   362
  
haftmann@15960
   363
  After this \verb!setup!,
haftmann@15960
   364
  there will be a new style available named \verb!new_lhs!, thus allowing
nipkow@15953
   365
  antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
nipkow@15953
   366
  yielding @{thm_style lhs rev_map}.
haftmann@15917
   367
haftmann@15917
   368
  The example above may be used as as a ``copy-and-paste'' pattern to write
haftmann@15917
   369
  your own styles; for a description of the constructs used, please refer
haftmann@15917
   370
  to the Isabelle reference manual.
haftmann@15917
   371
haftmann@15960
   372
haftmann@15917
   373
*}
haftmann@15917
   374
nipkow@15337
   375
(*<*)
nipkow@15337
   376
end
nipkow@15337
   377
(*>*)