diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/Document_Preparation.thy --- 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 "\"} @{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 "\"}~@{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 \ a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. + \item @{text "@{thm a\<^sub>1 \ a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. Full fact expressions are allowed here, including attributes (\secref{sec:syn-att}). - \item [@{text "@{prop \}"}] prints a well-typed proposition @{text + \item @{text "@{prop \}"} prints a well-typed proposition @{text "\"}. - \item [@{text "@{lemma \ by m}"}] proves a well-typed proposition + \item @{text "@{lemma \ by m}"} proves a well-typed proposition @{text "\"} by method @{text m} and prints the original @{text "\"}. - \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 \ x\<^sub>n}"}] prints a constant - abbreviation @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in - the current context. + \item @{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"} prints a constant abbreviation + @{text "c x\<^sub>1 \ x\<^sub>n \ 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 \}"}] prints a well-formed type @{text "\"}. + \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. - \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 \ a\<^sub>n}"}] prints the (compact) proof terms + \item @{text "@{prf a\<^sub>1 \ a\<^sub>n}"} prints the (compact) proof terms corresponding to the theorems @{text "a\<^sub>1 \ 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 \ a\<^sub>n}"}] is like @{text - "@{prf a\<^sub>1 \ 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 \ a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \ + 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 \ \ A\<^sub>n \ C"}. - \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise - number @{text "1, \, 9"}, respectively, from from a rule in - Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} + \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number + @{text "1, \, 9"}, respectively, from from a rule in Horn-clause + normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ 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 \}-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