--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:41:04 2008 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:43:46 2008 +0100
@@ -90,36 +90,36 @@
;
\end{rail}
- \begin{descr}
+ \begin{description}
- \item [@{command header}] provides plain text markup just preceding
+ \item @{command header} provides plain text markup just preceding
the formal beginning of a theory. The corresponding {\LaTeX} macro
is @{verbatim "\\isamarkupheader"}, which acts like @{command
section} by default.
- \item [@{command chapter}, @{command section}, @{command
- subsection}, and @{command subsubsection}] mark chapter and section
- headings within the main theory body or local theory targets. The
+ \item @{command chapter}, @{command section}, @{command subsection},
+ and @{command subsubsection} mark chapter and section headings
+ within the main theory body or local theory targets. The
corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"},
@{verbatim "\\isamarkupsection"}, @{verbatim
"\\isamarkupsubsection"} etc.
- \item [@{command sect}, @{command subsect}, and @{command
- subsubsect}] mark section headings within proofs. The corresponding
- {\LaTeX} macros are @{verbatim "\\isamarkupsect"}, @{verbatim
+ \item @{command sect}, @{command subsect}, and @{command subsubsect}
+ mark section headings within proofs. The corresponding {\LaTeX}
+ macros are @{verbatim "\\isamarkupsect"}, @{verbatim
"\\isamarkupsubsect"} etc.
- \item [@{command text} and @{command txt}] specify paragraphs of
- plain text. This corresponds to a {\LaTeX} environment @{verbatim
+ \item @{command text} and @{command txt} specify paragraphs of plain
+ text. This corresponds to a {\LaTeX} environment @{verbatim
"\\begin{isamarkuptext}"} @{text "\<dots>"} @{verbatim
"\\end{isamarkuptext}"} etc.
- \item [@{command text_raw} and @{command txt_raw}] insert {\LaTeX}
+ \item @{command text_raw} and @{command txt_raw} insert {\LaTeX}
source into the output, without additional markup. Thus the full
range of document manipulations becomes available, at the risk of
messing up document output.
- \end{descr}
+ \end{description}
Except for @{command "text_raw"} and @{command "txt_raw"}, the text
passed to any of the above markup commands may refer to formal
@@ -214,49 +214,48 @@
text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
"*"}@{verbatim "}"}.
- \begin{descr}
+ \begin{description}
- \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
+ \item @{text "@{theory A}"} prints the name @{text "A"}, which is
guaranteed to refer to a valid ancestor theory in the current
context.
- \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
+ \item @{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
Full fact expressions are allowed here, including attributes
(\secref{sec:syn-att}).
- \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
+ \item @{text "@{prop \<phi>}"} prints a well-typed proposition @{text
"\<phi>"}.
- \item [@{text "@{lemma \<phi> by m}"}] proves a well-typed proposition
+ \item @{text "@{lemma \<phi> by m}"} proves a well-typed proposition
@{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
- \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
+ \item @{text "@{term t}"} prints a well-typed term @{text "t"}.
- \item [@{text "@{const c}"}] prints a logical or syntactic constant
+ \item @{text "@{const c}"} prints a logical or syntactic constant
@{text "c"}.
- \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
- abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
- the current context.
+ \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
+ @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
- \item [@{text "@{typeof t}"}] prints the type of a well-typed term
+ \item @{text "@{typeof t}"} prints the type of a well-typed term
@{text "t"}.
- \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
+ \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
- \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
+ \item @{text "@{thm_style s a}"} prints theorem @{text a},
previously applying a style @{text s} to it (see below).
- \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
- t} after applying a style @{text s} to it (see below).
+ \item @{text "@{term_style s t}"} prints a well-typed term @{text t}
+ after applying a style @{text s} to it (see below).
- \item [@{text "@{text s}"}] prints uninterpreted source text @{text
+ \item @{text "@{text s}"} prints uninterpreted source text @{text
s}. This is particularly useful to print portions of text according
to the Isabelle document style, without demanding well-formedness,
e.g.\ small pieces of terms that should not be parsed or
type-checked yet.
- \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
+ \item @{text "@{goals}"} prints the current \emph{dynamic} goal
state. This is mainly for support of tactic-emulation scripts
within Isar. Presentation of goal states does not conform to the
idea of human-readable proof documents!
@@ -265,24 +264,24 @@
the reasoning via proper Isar proof commands, instead of peeking at
the internal machine configuration.
- \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
+ \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but
does not print the main goal.
- \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact) proof terms
+ \item @{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"} prints the (compact) proof terms
corresponding to the theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that this
requires proof terms to be switched on for the current logic
session.
- \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
- "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but prints the full proof terms, i.e.\ also
- displays information omitted in the compact proof term, which is
- denoted by ``@{text _}'' placeholders there.
+ \item @{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \<dots>
+ a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays
+ information omitted in the compact proof term, which is denoted by
+ ``@{text _}'' placeholders there.
- \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
- "@{ML_struct s}"}] check text @{text s} as ML value, type, and
+ \item @{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
+ "@{ML_struct s}"} check text @{text s} as ML value, type, and
structure, respectively. The source is printed verbatim.
- \end{descr}
+ \end{description}
*}
@@ -292,23 +291,23 @@
term_style} admit an extra \emph{style} specification to modify the
printed result. The following standard styles are available:
- \begin{descr}
+ \begin{description}
- \item [@{text lhs}] extracts the first argument of any application
+ \item @{text lhs} extracts the first argument of any application
form with at least two arguments --- typically meta-level or
object-level equality, or any other binary relation.
- \item [@{text rhs}] is like @{text lhs}, but extracts the second
+ \item @{text rhs} is like @{text lhs}, but extracts the second
argument.
- \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
+ \item @{text "concl"} extracts the conclusion @{text C} from a rule
in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
- \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
- number @{text "1, \<dots>, 9"}, respectively, from from a rule in
- Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
+ \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number
+ @{text "1, \<dots>, 9"}, respectively, from from a rule in Horn-clause
+ normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
- \end{descr}
+ \end{description}
*}
@@ -318,63 +317,63 @@
of antiquotations. Note that many of these coincide with global ML
flags of the same names.
- \begin{descr}
+ \begin{description}
- \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
+ \item @{text "show_types = bool"} and @{text "show_sorts = bool"}
control printing of explicit type and sort constraints.
- \item[@{text "show_structs = bool"}] controls printing of implicit
+ \item @{text "show_structs = bool"} controls printing of implicit
structures.
- \item[@{text "long_names = bool"}] forces names of types and
+ \item @{text "long_names = bool"} forces names of types and
constants etc.\ to be printed in their fully qualified internal
form.
- \item[@{text "short_names = bool"}] forces names of types and
+ \item @{text "short_names = bool"} forces names of types and
constants etc.\ to be printed unqualified. Note that internalizing
the output again in the current context may well yield a different
result.
- \item[@{text "unique_names = bool"}] determines whether the printed
+ \item @{text "unique_names = bool"} determines whether the printed
version of qualified names should be made sufficiently long to avoid
overlap with names declared further back. Set to @{text false} for
more concise output.
- \item[@{text "eta_contract = bool"}] prints terms in @{text
+ \item @{text "eta_contract = bool"} prints terms in @{text
\<eta>}-contracted form.
- \item[@{text "display = bool"}] indicates if the text is to be
- output as multi-line ``display material'', rather than a small piece
- of text without line breaks (which is the default).
+ \item @{text "display = bool"} indicates if the text is to be output
+ as multi-line ``display material'', rather than a small piece of
+ text without line breaks (which is the default).
In this mode the embedded entities are printed in the same style as
the main theory text.
- \item[@{text "break = bool"}] controls line breaks in non-display
+ \item @{text "break = bool"} controls line breaks in non-display
material.
- \item[@{text "quotes = bool"}] indicates if the output should be
+ \item @{text "quotes = bool"} indicates if the output should be
enclosed in double quotes.
- \item[@{text "mode = name"}] adds @{text name} to the print mode to
+ \item @{text "mode = name"} adds @{text name} to the print mode to
be used for presentation (see also \cite{isabelle-ref}). Note that
the standard setup for {\LaTeX} output is already present by
default, including the modes @{text latex} and @{text xsymbols}.
- \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
+ \item @{text "margin = nat"} and @{text "indent = nat"} change the
margin or indentation for pretty printing of display material.
- \item[@{text "goals_limit = nat"}] determines the maximum number of
+ \item @{text "goals_limit = nat"} determines the maximum number of
goals to be printed (for goal-based antiquotation).
- \item[@{text "locale = name"}] specifies an alternative locale
+ \item @{text "locale = name"} specifies an alternative locale
context used for evaluating and printing the subsequent argument.
- \item[@{text "source = bool"}] prints the original source text of
- the antiquotation arguments, rather than its internal
- representation. Note that formal checking of @{antiquotation
- "thm"}, @{antiquotation "term"}, etc. is still enabled; use the
- @{antiquotation "text"} antiquotation for unchecked output.
+ \item @{text "source = bool"} prints the original source text of the
+ antiquotation arguments, rather than its internal representation.
+ Note that formal checking of @{antiquotation "thm"}, @{antiquotation
+ "term"}, etc. is still enabled; use the @{antiquotation "text"}
+ antiquotation for unchecked output.
Regular @{text "term"} and @{text "typ"} antiquotations with @{text
"source = false"} involve a full round-trip from the original source
@@ -387,7 +386,7 @@
given source text, with the desirable well-formedness check in the
background, but without modification of the printed text.
- \end{descr}
+ \end{description}
For boolean flags, ``@{text "name = true"}'' may be abbreviated as
``@{text name}''. All of the above flags are disabled by default,
@@ -462,15 +461,15 @@
;
\end{rail}
- \begin{descr}
+ \begin{description}
- \item [@{command "display_drafts"}~@{text paths} and @{command
- "print_drafts"}~@{text paths}] perform simple output of a given list
+ \item @{command "display_drafts"}~@{text paths} and @{command
+ "print_drafts"}~@{text paths} perform simple output of a given list
of raw source files. Only those symbols that do not require
additional {\LaTeX} packages are displayed properly, everything else
is left verbatim.
- \end{descr}
+ \end{description}
*}
end