diff -r 151f894984d8 -r 2bf52eec4e8a src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed Oct 14 15:06:42 2015 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed Oct 14 15:10:32 2015 +0200 @@ -51,19 +51,19 @@ \begin{description} - \item @{command chapter}, @{command section}, @{command subsection}, and + \<^descr> @{command chapter}, @{command section}, @{command subsection}, and @{command subsubsection} mark chapter and section headings within the theory source; this works in any context, even before the initial @{command theory} command. The corresponding {\LaTeX} macros are @{verbatim \\isamarkupchapter\}, @{verbatim \\isamarkupsection\}, @{verbatim \\isamarkupsubsection\}, @{verbatim \\isamarkupsubsubsection\}. - \item @{command text} and @{command txt} specify paragraphs of plain text. + \<^descr> @{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} inserts {\LaTeX} source directly into the + \<^descr> @{command text_raw} inserts {\LaTeX} source directly into the output, without additional markup. Thus the full range of document manipulations becomes available, at the risk of messing up document output. @@ -189,55 +189,55 @@ \begin{description} - \item @{command "print_antiquotations"} prints all document antiquotations + \<^descr> @{command "print_antiquotations"} prints all document antiquotations that are defined in the current context; the ``@{text "!"}'' option indicates extra verbosity. - \item @{text "@{theory A}"} prints the name @{text "A"}, which is + \<^descr> @{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"}. + \<^descr> @{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 + \<^descr> @{text "@{prop \}"} prints a well-typed proposition @{text "\"}. - \item @{text "@{lemma \ by m}"} proves a well-typed proposition + \<^descr> @{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"}. + \<^descr> @{text "@{term t}"} prints a well-typed term @{text "t"}. - \item @{text "@{value t}"} evaluates a term @{text "t"} and prints + \<^descr> @{text "@{value t}"} evaluates a term @{text "t"} and prints its result, see also @{command_ref (HOL) value}. - \item @{text "@{term_type t}"} prints a well-typed term @{text "t"} + \<^descr> @{text "@{term_type t}"} prints a well-typed term @{text "t"} annotated with its type. - \item @{text "@{typeof t}"} prints the type of a well-typed term + \<^descr> @{text "@{typeof t}"} prints the type of a well-typed term @{text "t"}. - \item @{text "@{const c}"} prints a logical or syntactic constant + \<^descr> @{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 + \<^descr> @{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 "@{typ \}"} prints a well-formed type @{text "\"}. + \<^descr> @{text "@{typ \}"} prints a well-formed type @{text "\"}. - \item @{text "@{type \}"} prints a (logical or syntactic) type + \<^descr> @{text "@{type \}"} prints a (logical or syntactic) type constructor @{text "\"}. - \item @{text "@{class c}"} prints a class @{text c}. + \<^descr> @{text "@{class c}"} prints a class @{text c}. - \item @{text "@{text s}"} prints uninterpreted source text @{text + \<^descr> @{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 + \<^descr> @{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! @@ -246,38 +246,38 @@ the reasoning via proper Isar proof commands, instead of peeking at the internal machine configuration. - \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but + \<^descr> @{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 + \<^descr> @{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 \ + \<^descr> @{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_op s}"}, @{text "@{ML_type + \<^descr> @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type s}"}, @{text "@{ML_structure s}"}, and @{text "@{ML_functor s}"} check text @{text s} as ML value, infix operator, type, structure, and functor respectively. The source is printed verbatim. - \item @{text "@{verbatim s}"} prints uninterpreted source text literally + \<^descr> @{text "@{verbatim s}"} prints uninterpreted source text literally as ASCII characters, using some type-writer font style. - \item @{text "@{file path}"} checks that @{text "path"} refers to a + \<^descr> @{text "@{file path}"} checks that @{text "path"} refers to a file (or directory) and prints it verbatim. - \item @{text "@{file_unchecked path}"} is like @{text "@{file + \<^descr> @{text "@{file_unchecked path}"} is like @{text "@{file path}"}, but does not check the existence of the @{text "path"} within the file-system. - \item @{text "@{url name}"} produces markup for the given URL, which + \<^descr> @{text "@{url name}"} produces markup for the given URL, which results in an active hyperlink within the text. - \item @{text "@{cite name}"} produces a citation @{verbatim + \<^descr> @{text "@{cite name}"} produces a citation @{verbatim \\cite{name}\} in {\LaTeX}, where the name refers to some Bib{\TeX} database entry. @@ -305,17 +305,17 @@ \begin{description} - \item @{text lhs} extracts the first argument of any application + \<^descr> @{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 + \<^descr> @{text rhs} is like @{text lhs}, but extracts the second argument. - \item @{text "concl"} extracts the conclusion @{text C} from a rule + \<^descr> @{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 "prem"} @{text n} extract premise number + \<^descr> @{text "prem"} @{text n} extract premise number @{text "n"} from from a rule in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} @@ -331,34 +331,34 @@ \begin{description} - \item @{antiquotation_option_def show_types}~@{text "= bool"} and + \<^descr> @{antiquotation_option_def show_types}~@{text "= bool"} and @{antiquotation_option_def show_sorts}~@{text "= bool"} control printing of explicit type and sort constraints. - \item @{antiquotation_option_def show_structs}~@{text "= bool"} + \<^descr> @{antiquotation_option_def show_structs}~@{text "= bool"} controls printing of implicit structures. - \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"} + \<^descr> @{antiquotation_option_def show_abbrevs}~@{text "= bool"} controls folding of abbreviations. - \item @{antiquotation_option_def names_long}~@{text "= bool"} forces + \<^descr> @{antiquotation_option_def names_long}~@{text "= bool"} forces names of types and constants etc.\ to be printed in their fully qualified internal form. - \item @{antiquotation_option_def names_short}~@{text "= bool"} + \<^descr> @{antiquotation_option_def names_short}~@{text "= 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 @{antiquotation_option_def names_unique}~@{text "= bool"} + \<^descr> @{antiquotation_option_def names_unique}~@{text "= 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 @{antiquotation_option_def eta_contract}~@{text "= bool"} + \<^descr> @{antiquotation_option_def eta_contract}~@{text "= bool"} prints terms in @{text \}-contracted form. - \item @{antiquotation_option_def display}~@{text "= bool"} indicates + \<^descr> @{antiquotation_option_def display}~@{text "= 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). @@ -366,26 +366,26 @@ In this mode the embedded entities are printed in the same style as the main theory text. - \item @{antiquotation_option_def break}~@{text "= bool"} controls + \<^descr> @{antiquotation_option_def break}~@{text "= bool"} controls line breaks in non-display material. - \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates + \<^descr> @{antiquotation_option_def quotes}~@{text "= bool"} indicates if the output should be enclosed in double quotes. - \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text + \<^descr> @{antiquotation_option_def mode}~@{text "= name"} adds @{text name} to the print mode to be used for presentation. Note that the standard setup for {\LaTeX} output is already present by default, including the modes @{text latex} and @{text xsymbols}. - \item @{antiquotation_option_def margin}~@{text "= nat"} and + \<^descr> @{antiquotation_option_def margin}~@{text "= nat"} and @{antiquotation_option_def indent}~@{text "= nat"} change the margin or indentation for pretty printing of display material. - \item @{antiquotation_option_def goals_limit}~@{text "= nat"} + \<^descr> @{antiquotation_option_def goals_limit}~@{text "= nat"} determines the maximum number of subgoals to be printed (for goal-based antiquotation). - \item @{antiquotation_option_def source}~@{text "= bool"} prints the + \<^descr> @{antiquotation_option_def source}~@{text "= 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 @@ -592,7 +592,7 @@ \begin{description} - \item @{command "display_drafts"}~@{text paths} performs simple output of a + \<^descr> @{command "display_drafts"}~@{text paths} performs 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.