1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:41:04 2008 +0100
1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:43:46 2008 +0100
1.3 @@ -90,36 +90,36 @@
1.4 ;
1.5 \end{rail}
1.6
1.7 - \begin{descr}
1.8 + \begin{description}
1.9
1.10 - \item [@{command header}] provides plain text markup just preceding
1.11 + \item @{command header} provides plain text markup just preceding
1.12 the formal beginning of a theory. The corresponding {\LaTeX} macro
1.13 is @{verbatim "\\isamarkupheader"}, which acts like @{command
1.14 section} by default.
1.15
1.16 - \item [@{command chapter}, @{command section}, @{command
1.17 - subsection}, and @{command subsubsection}] mark chapter and section
1.18 - headings within the main theory body or local theory targets. The
1.19 + \item @{command chapter}, @{command section}, @{command subsection},
1.20 + and @{command subsubsection} mark chapter and section headings
1.21 + within the main theory body or local theory targets. The
1.22 corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"},
1.23 @{verbatim "\\isamarkupsection"}, @{verbatim
1.24 "\\isamarkupsubsection"} etc.
1.25
1.26 - \item [@{command sect}, @{command subsect}, and @{command
1.27 - subsubsect}] mark section headings within proofs. The corresponding
1.28 - {\LaTeX} macros are @{verbatim "\\isamarkupsect"}, @{verbatim
1.29 + \item @{command sect}, @{command subsect}, and @{command subsubsect}
1.30 + mark section headings within proofs. The corresponding {\LaTeX}
1.31 + macros are @{verbatim "\\isamarkupsect"}, @{verbatim
1.32 "\\isamarkupsubsect"} etc.
1.33
1.34 - \item [@{command text} and @{command txt}] specify paragraphs of
1.35 - plain text. This corresponds to a {\LaTeX} environment @{verbatim
1.36 + \item @{command text} and @{command txt} specify paragraphs of plain
1.37 + text. This corresponds to a {\LaTeX} environment @{verbatim
1.38 "\\begin{isamarkuptext}"} @{text "\<dots>"} @{verbatim
1.39 "\\end{isamarkuptext}"} etc.
1.40
1.41 - \item [@{command text_raw} and @{command txt_raw}] insert {\LaTeX}
1.42 + \item @{command text_raw} and @{command txt_raw} insert {\LaTeX}
1.43 source into the output, without additional markup. Thus the full
1.44 range of document manipulations becomes available, at the risk of
1.45 messing up document output.
1.46
1.47 - \end{descr}
1.48 + \end{description}
1.49
1.50 Except for @{command "text_raw"} and @{command "txt_raw"}, the text
1.51 passed to any of the above markup commands may refer to formal
1.52 @@ -214,49 +214,48 @@
1.53 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
1.54 "*"}@{verbatim "}"}.
1.55
1.56 - \begin{descr}
1.57 + \begin{description}
1.58
1.59 - \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
1.60 + \item @{text "@{theory A}"} prints the name @{text "A"}, which is
1.61 guaranteed to refer to a valid ancestor theory in the current
1.62 context.
1.63
1.64 - \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
1.65 + \item @{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
1.66 Full fact expressions are allowed here, including attributes
1.67 (\secref{sec:syn-att}).
1.68
1.69 - \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
1.70 + \item @{text "@{prop \<phi>}"} prints a well-typed proposition @{text
1.71 "\<phi>"}.
1.72
1.73 - \item [@{text "@{lemma \<phi> by m}"}] proves a well-typed proposition
1.74 + \item @{text "@{lemma \<phi> by m}"} proves a well-typed proposition
1.75 @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
1.76
1.77 - \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
1.78 + \item @{text "@{term t}"} prints a well-typed term @{text "t"}.
1.79
1.80 - \item [@{text "@{const c}"}] prints a logical or syntactic constant
1.81 + \item @{text "@{const c}"} prints a logical or syntactic constant
1.82 @{text "c"}.
1.83
1.84 - \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
1.85 - abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
1.86 - the current context.
1.87 + \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
1.88 + @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
1.89
1.90 - \item [@{text "@{typeof t}"}] prints the type of a well-typed term
1.91 + \item @{text "@{typeof t}"} prints the type of a well-typed term
1.92 @{text "t"}.
1.93
1.94 - \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
1.95 + \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
1.96
1.97 - \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
1.98 + \item @{text "@{thm_style s a}"} prints theorem @{text a},
1.99 previously applying a style @{text s} to it (see below).
1.100
1.101 - \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
1.102 - t} after applying a style @{text s} to it (see below).
1.103 + \item @{text "@{term_style s t}"} prints a well-typed term @{text t}
1.104 + after applying a style @{text s} to it (see below).
1.105
1.106 - \item [@{text "@{text s}"}] prints uninterpreted source text @{text
1.107 + \item @{text "@{text s}"} prints uninterpreted source text @{text
1.108 s}. This is particularly useful to print portions of text according
1.109 to the Isabelle document style, without demanding well-formedness,
1.110 e.g.\ small pieces of terms that should not be parsed or
1.111 type-checked yet.
1.112
1.113 - \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
1.114 + \item @{text "@{goals}"} prints the current \emph{dynamic} goal
1.115 state. This is mainly for support of tactic-emulation scripts
1.116 within Isar. Presentation of goal states does not conform to the
1.117 idea of human-readable proof documents!
1.118 @@ -265,24 +264,24 @@
1.119 the reasoning via proper Isar proof commands, instead of peeking at
1.120 the internal machine configuration.
1.121
1.122 - \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
1.123 + \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but
1.124 does not print the main goal.
1.125
1.126 - \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact) proof terms
1.127 + \item @{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"} prints the (compact) proof terms
1.128 corresponding to the theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that this
1.129 requires proof terms to be switched on for the current logic
1.130 session.
1.131
1.132 - \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
1.133 - "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but prints the full proof terms, i.e.\ also
1.134 - displays information omitted in the compact proof term, which is
1.135 - denoted by ``@{text _}'' placeholders there.
1.136 + \item @{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \<dots>
1.137 + a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays
1.138 + information omitted in the compact proof term, which is denoted by
1.139 + ``@{text _}'' placeholders there.
1.140
1.141 - \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
1.142 - "@{ML_struct s}"}] check text @{text s} as ML value, type, and
1.143 + \item @{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
1.144 + "@{ML_struct s}"} check text @{text s} as ML value, type, and
1.145 structure, respectively. The source is printed verbatim.
1.146
1.147 - \end{descr}
1.148 + \end{description}
1.149 *}
1.150
1.151
1.152 @@ -292,23 +291,23 @@
1.153 term_style} admit an extra \emph{style} specification to modify the
1.154 printed result. The following standard styles are available:
1.155
1.156 - \begin{descr}
1.157 + \begin{description}
1.158
1.159 - \item [@{text lhs}] extracts the first argument of any application
1.160 + \item @{text lhs} extracts the first argument of any application
1.161 form with at least two arguments --- typically meta-level or
1.162 object-level equality, or any other binary relation.
1.163
1.164 - \item [@{text rhs}] is like @{text lhs}, but extracts the second
1.165 + \item @{text rhs} is like @{text lhs}, but extracts the second
1.166 argument.
1.167
1.168 - \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
1.169 + \item @{text "concl"} extracts the conclusion @{text C} from a rule
1.170 in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
1.171
1.172 - \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
1.173 - number @{text "1, \<dots>, 9"}, respectively, from from a rule in
1.174 - Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
1.175 + \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number
1.176 + @{text "1, \<dots>, 9"}, respectively, from from a rule in Horn-clause
1.177 + normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
1.178
1.179 - \end{descr}
1.180 + \end{description}
1.181 *}
1.182
1.183
1.184 @@ -318,63 +317,63 @@
1.185 of antiquotations. Note that many of these coincide with global ML
1.186 flags of the same names.
1.187
1.188 - \begin{descr}
1.189 + \begin{description}
1.190
1.191 - \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
1.192 + \item @{text "show_types = bool"} and @{text "show_sorts = bool"}
1.193 control printing of explicit type and sort constraints.
1.194
1.195 - \item[@{text "show_structs = bool"}] controls printing of implicit
1.196 + \item @{text "show_structs = bool"} controls printing of implicit
1.197 structures.
1.198
1.199 - \item[@{text "long_names = bool"}] forces names of types and
1.200 + \item @{text "long_names = bool"} forces names of types and
1.201 constants etc.\ to be printed in their fully qualified internal
1.202 form.
1.203
1.204 - \item[@{text "short_names = bool"}] forces names of types and
1.205 + \item @{text "short_names = bool"} forces names of types and
1.206 constants etc.\ to be printed unqualified. Note that internalizing
1.207 the output again in the current context may well yield a different
1.208 result.
1.209
1.210 - \item[@{text "unique_names = bool"}] determines whether the printed
1.211 + \item @{text "unique_names = bool"} determines whether the printed
1.212 version of qualified names should be made sufficiently long to avoid
1.213 overlap with names declared further back. Set to @{text false} for
1.214 more concise output.
1.215
1.216 - \item[@{text "eta_contract = bool"}] prints terms in @{text
1.217 + \item @{text "eta_contract = bool"} prints terms in @{text
1.218 \<eta>}-contracted form.
1.219
1.220 - \item[@{text "display = bool"}] indicates if the text is to be
1.221 - output as multi-line ``display material'', rather than a small piece
1.222 - of text without line breaks (which is the default).
1.223 + \item @{text "display = bool"} indicates if the text is to be output
1.224 + as multi-line ``display material'', rather than a small piece of
1.225 + text without line breaks (which is the default).
1.226
1.227 In this mode the embedded entities are printed in the same style as
1.228 the main theory text.
1.229
1.230 - \item[@{text "break = bool"}] controls line breaks in non-display
1.231 + \item @{text "break = bool"} controls line breaks in non-display
1.232 material.
1.233
1.234 - \item[@{text "quotes = bool"}] indicates if the output should be
1.235 + \item @{text "quotes = bool"} indicates if the output should be
1.236 enclosed in double quotes.
1.237
1.238 - \item[@{text "mode = name"}] adds @{text name} to the print mode to
1.239 + \item @{text "mode = name"} adds @{text name} to the print mode to
1.240 be used for presentation (see also \cite{isabelle-ref}). Note that
1.241 the standard setup for {\LaTeX} output is already present by
1.242 default, including the modes @{text latex} and @{text xsymbols}.
1.243
1.244 - \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
1.245 + \item @{text "margin = nat"} and @{text "indent = nat"} change the
1.246 margin or indentation for pretty printing of display material.
1.247
1.248 - \item[@{text "goals_limit = nat"}] determines the maximum number of
1.249 + \item @{text "goals_limit = nat"} determines the maximum number of
1.250 goals to be printed (for goal-based antiquotation).
1.251
1.252 - \item[@{text "locale = name"}] specifies an alternative locale
1.253 + \item @{text "locale = name"} specifies an alternative locale
1.254 context used for evaluating and printing the subsequent argument.
1.255
1.256 - \item[@{text "source = bool"}] prints the original source text of
1.257 - the antiquotation arguments, rather than its internal
1.258 - representation. Note that formal checking of @{antiquotation
1.259 - "thm"}, @{antiquotation "term"}, etc. is still enabled; use the
1.260 - @{antiquotation "text"} antiquotation for unchecked output.
1.261 + \item @{text "source = bool"} prints the original source text of the
1.262 + antiquotation arguments, rather than its internal representation.
1.263 + Note that formal checking of @{antiquotation "thm"}, @{antiquotation
1.264 + "term"}, etc. is still enabled; use the @{antiquotation "text"}
1.265 + antiquotation for unchecked output.
1.266
1.267 Regular @{text "term"} and @{text "typ"} antiquotations with @{text
1.268 "source = false"} involve a full round-trip from the original source
1.269 @@ -387,7 +386,7 @@
1.270 given source text, with the desirable well-formedness check in the
1.271 background, but without modification of the printed text.
1.272
1.273 - \end{descr}
1.274 + \end{description}
1.275
1.276 For boolean flags, ``@{text "name = true"}'' may be abbreviated as
1.277 ``@{text name}''. All of the above flags are disabled by default,
1.278 @@ -462,15 +461,15 @@
1.279 ;
1.280 \end{rail}
1.281
1.282 - \begin{descr}
1.283 + \begin{description}
1.284
1.285 - \item [@{command "display_drafts"}~@{text paths} and @{command
1.286 - "print_drafts"}~@{text paths}] perform simple output of a given list
1.287 + \item @{command "display_drafts"}~@{text paths} and @{command
1.288 + "print_drafts"}~@{text paths} perform simple output of a given list
1.289 of raw source files. Only those symbols that do not require
1.290 additional {\LaTeX} packages are displayed properly, everything else
1.291 is left verbatim.
1.292
1.293 - \end{descr}
1.294 + \end{description}
1.295 *}
1.296
1.297 end