(*:maxLineLen=78:*) theory Document_Preparationimports Main Basebegin chapter ‹ Document preparation \label {ch:document-prep}› text ‹ \LaTeX }, with support for hyperlinks and bookmarks within that format.\ from Isabelle theory\LaTeX } output is generated while processing a 🪙 ‹ session› in batch mode, as🪙 ‹ The Isabelle System Manual› cite ‹ "isabelle-system"› .cite ‹ "isabelle-hol-book"› also explains› section ‹ Markup commands \label {sec:markup}› text ‹ \begin {matharray}{rcl}‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ ‹ any → any› \\ \end {matharray}\LaTeX } macro. The🍋 ‹ ~~/lib/texinputs/isabelle.sty› can be\LaTeX }\secref {sec:comments}) are similar to markup🪙 ‹ › 🪙 @{command chapter}, @{command section}, @{command subsection} etc.\ mark\LaTeX }🍋 ‹ \isamarkupchapter › , 🍋 ‹ \isamarkupsection › ,acro" is null🪙 @{command text} and @{command txt} specify paragraphs of plain text.\LaTeX } environment 🍋 ‹ \begin {isamarkuptext}› ‹ … › 🍋 ‹ \end {isamarkuptext}› etc.🪙 @{command text_raw} is similar to @{command text}, but without any\LaTeX }🪙 ‹ document antiquotations› , see also \secref {sec:antiq}. These🪙 \LaTeX } macros. › section ‹ Document antiquotations \label {sec:antiq}› text ‹ \begin {matharray}{rcl}‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ \end {matharray}\begin {matharray}{rcl}‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ antiquotation› \\ ‹ * › & : & ‹ context → › \\ \end {matharray}\secref {sec:markup}) or\secref {sec:comments}). The argument of markup commands🪙 ‹ document antiquotations› .🍋 ‹ @{term [show_types] "f x = a + x"}› \isa {{\isacharparenleft }f{\isasymColon }{\isacharprime }a\ {\isasymRightarrow }\ {\isacharprime }a{\isacharparenright }\ {\isacharparenleft }x{\isasymColon }{\isacharprime }a{\isacharparenright }\ {\isacharequal }\ {\isacharparenleft }a{\isasymColon }{\isacharprime }a{\isacharparenright }\ {\isacharplus }\ x} appear in the final {\LaTeX } document.🪙 🍋 ‹ @{› ‹ name› ~🍋 ‹ [› ‹ options› 🍋 ‹ ]› ~‹ arguments› 🍋 ‹ }› . The short form🍋 ‹ \\ › 🍋 ‹ <^\<close>‹ name› 🍋 ‹ >› ‹ ‹ argument_content› › (without surrounding 🍋 ‹ @{› ‹ … › ?? ‹ }› )🍋 ‹ 🪙 › ‹ ‹ argument_content› › , which is🍋 ‹ @{cartouche› ~‹ ‹ argument_content› › 🍋 ‹ }› . The special name‹ ‹ foo_bar + baz ≤ bazar› › prints literal quasi-formal text🍋 ‹ \\ › 🍋 ‹ <^\<close>‹ name› 🍋 ‹ >› within the body text, but🍋 ‹ @{› ‹ name› 🍋 ‹ }› .\begingroup \def \isasymcontrolstart {\isatt {\isacharbackslash \isacharless \isacharcircum }}🪙 ‹ 🪙 ' @{syntax_ref name} '>' @{syntax_ref cartouche} |› \endgroup 🪙 ‹ not› include source comments › nor verbatim text 🍋 ‹ {*› ~‹ … › ~🍋 ‹ *}› . % % FIXME less monolithic presentation , move to individual sections ! ? \ < ^ rail > \ < open > @ { syntax_def antiquotation_body } : ( @ @ { antiquotation text } | @ @ { antiquotation cartouche } | @ @ { antiquotation theory_text } ) options @ { syntax text } | @ @ { antiquotation theory } options @ { syntax embedded } | @ @ { antiquotation thm } options styles @ { syntax thms } | @ @ { antiquotation lemma } options @ { syntax prop } @ ' by ' @ { syntax method } @ { syntax method } ? | @ @ { antiquotation prop } options styles @ { syntax prop } | @ @ { antiquotation term } options styles @ { syntax term } | @ @ { antiquotation ( HOL ) value } options styles @ { syntax term } | @ @ { antiquotation term_type } options styles @ { syntax term } | @ @ { antiquotation typeof } options styles @ { syntax term } | @ @ { antiquotation const } options @ { syntax term } | @ @ { antiquotation abbrev } options @ { syntax term } | @ @ { antiquotation typ } options @ { syntax type } | @ @ { antiquotation type } options @ { syntax embedded } | @ @ { antiquotation class } options @ { syntax embedded } | @ @ { antiquotation locale } options @ { syntax embedded } | @ @ { antiquotation bundle } options @ { syntax embedded } | ( @ @ { antiquotation command } | @ @ { antiquotation method } | @ @ { antiquotation attribute } ) options @ { syntax name } ; @ { syntax antiquotation } : @ @ { antiquotation goals } options | @ @ { antiquotation subgoals } options | @ @ { antiquotation prf } options @ { syntax thms } | @ @ { antiquotation full_prf } options @ { syntax thms } | @ @ { antiquotation ML_text } options @ { syntax text } | @ @ { antiquotation ML } options @ { syntax text } | @ @ { antiquotation ML_infix } options @ { syntax text } | @ @ { antiquotation ML_type } options @ { syntax typeargs } @ { syntax text } | @ @ { antiquotation ML_structure } options @ { syntax text } | @ @ { antiquotation ML_functor } options @ { syntax text } | @ @ { antiquotation emph } options @ { syntax text } | @ @ { antiquotation bold } options @ { syntax text } | @ @ { antiquotation verbatim } options @ { syntax text } | @ @ { antiquotation bash_function } options @ { syntax embedded } | @ @ { antiquotation system_option } options @ { syntax embedded } | @ @ { antiquotation session } options @ { syntax embedded } | @ @ { antiquotation path } options @ { syntax embedded } | @ @ { antiquotation " file " } options @ { syntax name } | @ @ { antiquotation dir } options @ { syntax name } | @ @ { antiquotation url } options @ { syntax embedded } | ( @ @ { antiquotation cite } | @ @ { antiquotation nocite } | @ @ { antiquotation citet } | @ @ { antiquotation citep } ) @ { syntax embedded } ; styles : ' ( ' ( style + ' , ' ) ' ) ' ; style : ( @ { syntax name } + ) ; @ @ { command print_antiquotations } ( ' ! ' ? ) \ < close > \ < ^ descr > \ < open > @ { text s } \ < close > prints uninterpreted source text \ < open > s \ < close > , i . e . \ inner syntax . 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 . It is also possible to write this in the short form \ < open > \ < open > s \ < close > \ < close > without any further decoration . \ < ^ descr > \ < open > @ { theory_text s } \ < close > prints uninterpreted theory source text \ < open > s \ < close > , i . e . \ outer syntax with command keywords and other tokens . \ < ^ descr > \ < open > @ { theory A } \ < close > prints the session - qualified theory name \ < open > A \ < close > , which is guaranteed to refer to a valid ancestor theory in the current context . \ < ^ descr > \ < open > @ { thm a \ < ^ sub > 1 \ < dots > a \ < ^ sub > n } \ < close > prints theorems \ < open > a \ < ^ sub > 1 \ < dots > a \ < ^ sub > n \ < close > . Full fact expressions are allowed here , including attributes ( \ secref { sec : syn - att } ) . \ < ^ descr > \ < open > @ { prop \ < phi > } \ < close > prints a well - typed proposition \ < open > \ < phi > \ < close > . \ < ^ descr > \ < open > @ { lemma \ < phi > by m } \ < close > proves a well - typed proposition \ < open > \ < phi > \ < close > by method \ < open > m \ < close > and prints the original \ < open > \ < phi > \ < close > . \ < ^ descr > \ < open > @ { term t } \ < close > prints a well - typed term \ < open > t \ < close > . \ < ^ descr > \ < open > @ { value t } \ < close > evaluates a term \ < open > t \ < close > and prints its result , see also @ { command_ref ( HOL ) value } . \ < ^ descr > \ < open > @ { term_type t } \ < close > prints a well - typed term \ < open > t \ < close > annotated with its type . \ < ^ descr > \ < open > @ { typeof t } \ < close > prints the type of a well - typed term \ < open > t \ < close > . \ < ^ descr > \ < open > @ { const c } \ < close > prints a logical or syntactic constant \ < open > c \ < close > . \ < ^ descr > \ < open > @ { abbrev c x \ < ^ sub > 1 \ < dots > x \ < ^ sub > n } \ < close > prints a constant abbreviation \ < open > c x \ < ^ sub > 1 \ < dots > x \ < ^ sub > n \ < equiv > rhs \ < close > as defined in the current context . \ < ^ descr > \ < open > @ { typ \ < tau > } \ < close > prints a well - formed type \ < open > \ < tau > \ < close > . \ < ^ descr > \ < open > @ { type \ < kappa > } \ < close > prints a ( logical or syntactic ) type constructor \ < open > \ < kappa > \ < close > . \ < ^ descr > \ < open > @ { class c } \ < close > prints a class \ < open > c \ < close > . \ < ^ descr > \ < open > @ { locale c } \ < close > prints a locale \ < open > c \ < close > . \ < ^ descr > \ < open > @ { bundle c } \ < close > prints a bundle \ < open > c \ < close > . \ < ^ descr > \ < open > @ { command name } \ < close > , \ < open > @ { method name } \ < close > , \ < open > @ { attribute name } \ < close > print checked entities of the Isar language . \ < ^ descr > \ < open > @ { goals } \ < close > prints the current \ < ^ emph > \ < open > dynamic \ < close > 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 ! When explaining proofs in detail it is usually better to spell out the reasoning via proper Isar proof commands , instead of peeking at the internal machine configuration . \ < ^ descr > \ < open > @ { subgoals } \ < close > is similar to \ < open > @ { goals } \ < close > , but does not print the main goal . \ < ^ descr > \ < open > @ { prf a \ < ^ sub > 1 \ < dots > a \ < ^ sub > n } \ < close > prints the ( compact ) proof terms corresponding to the theorems \ < open > a \ < ^ sub > 1 \ < dots > a \ < ^ sub > n \ < close > . Note that this requires proof terms to be switched on for the current logic session . \ < ^ descr > \ < open > @ { full_prf a \ < ^ sub > 1 \ < dots > a \ < ^ sub > n } \ < close > is like \ < open > @ { prf a \ < ^ sub > 1 \ < dots > a \ < ^ sub > n } \ < close > , but prints the full proof terms , i . e . \ also displays information omitted in the compact proof term , which is denoted by ` ` \ < open > _ \ < close > ' ' placeholders there . \ < ^ descr > \ < open > @ { ML_text s } \ < close > prints ML text verbatim : only the token language is checked . \ < ^ descr > \ < open > @ { ML s } \ < close > , \ < open > @ { ML_infix s } \ < close > , \ < open > @ { ML_type s } \ < close > , \ < open > @ { ML_structure s } \ < close > , and \ < open > @ { ML_functor s } \ < close > check text \ < open > s \ < close > as ML value , infix operator , type , exception , structure , and functor respectively . The source is printed verbatim . The variants \ < open > @ { ML_def s } \ < close > and \ < open > @ { ML_ref s } \ < close > etc . maintain the document index : ` ` def ' ' means to make a bold entry , ` ` ref ' ' means to make a regular entry . There are two forms for type constructors , with or without separate type arguments : this impacts only the index entry . For example , \ < open > @ { ML_type_ref \ < open > ' a list \ < close > } \ < close > makes an entry literally for ` ` \ < open > ' a list \ < close > ' ' ( sorted under the letter ` ` a ' ' ) , but \ < open > @ { ML_type_ref ' a \ < open > list \ < close > } \ < close > makes an entry for the constructor name ` ` \ < open > list \ < close > ' ' . \ < ^ descr > \ < open > @ { emph s } \ < close > prints document source recursively , with { \ LaTeX } markup \ < ^ verbatim > \ < open > \ emph { \ < close > \ < open > \ < dots > \ < close > \ < ^ verbatim > \ < open > } \ < close > . \ < ^ descr > \ < open > @ { bold s } \ < close > prints document source recursively , with { \ LaTeX } markup \ < ^ verbatim > \ < open > \ textbf { \ < close > \ < open > \ < dots > \ < close > \ < ^ verbatim > \ < open > } \ < close > . \ < ^ descr > \ < open > @ { verbatim s } \ < close > prints uninterpreted source text literally as ASCII characters , using some type - writer font style . \ < ^ descr > \ < open > @ { bash_function name } \ < close > prints the given GNU bash function verbatim . The name is checked wrt . \ the Isabelle system environment \ < ^ cite > \ < open > " isabelle - system " \ < close > . \ < ^ descr > \ < open > @ { system_option name } \ < close > prints the given system option verbatim . The name is checked wrt . \ cumulative \ < ^ verbatim > \ < open > etc / options \ < close > of all Isabelle components , notably \ < ^ file > \ < open > ~ ~ / etc / options \ < close > . \ < ^ descr > \ < open > @ { session name } \ < close > prints given session name verbatim . The name is checked wrt . \ the dependencies of the current session . \ < ^ descr > \ < open > @ { path name } \ < close > prints the file - system path name verbatim . \ < ^ descr > \ < open > @ { file name } \ < close > is like \ < open > @ { path name } \ < close > , but ensures that \ < open > name \ < close > refers to a plain file . \ < ^ descr > \ < open > @ { dir name } \ < close > is like \ < open > @ { path name } \ < close > , but ensures that \ < open > name \ < close > refers to a directory . \ < ^ descr > \ < open > @ { url name } \ < close > produces markup for the given URL , which results in an active hyperlink within the text . \ < ^ descr > \ < open > @ { cite arg } \ < close > produces the Bib { \ TeX } citation macro \ < ^ verbatim > \ < open > \ cite [ . . . ] { . . . } \ < close > with its optional and mandatory argument . The analogous \ < ^ verbatim > \ < open > \ nocite \ < close > , and the \ < ^ verbatim > \ < open > \ citet \ < close > and \ < ^ verbatim > \ < open > \ citep \ < close > variants from the \ < ^ verbatim > \ < open > natbib \ < close > package \ < ^ footnote > \ < open > \ < ^ url > \ < open > https : / / ctan . org / pkg / natbib \ < close > \ < close > are supported as well . The argument syntax is uniform for all variants and is usually presented in control - symbol - cartouche form : \ < open > \ < ^ cite > \ < open > arg \ < close > \ < close > . The formal syntax of the nested argument language is defined as follows : \ < ^ rail > \ < open > arg : ( embedded @ ' in ' ) ? ( name + @ ' and ' ) \ < newline > ( @ ' using ' name ) ? \ < close > Here the embedded text is free - form { \ LaTeX } , which becomes the optional argument of the \ < ^ verbatim > \ < open > \ cite \ < close > macro . The named items are Bib { \ TeX } database entries and become the mandatory argument ( separated by comma ) . The optional part ` ` \ < ^ theory_text > \ < open > using name \ < close > ' ' specifies an alternative { \ LaTeX } macro name . \ < ^ descr > @ { command " print_antiquotations " } prints all document antiquotations that are defined in the current context ; the ` ` \ < open > ! \ < close > ' ' option indicates extra verbosity . \ < close > subsection \ < open > Styled antiquotations \ < close > text \ < open > The antiquotations \ < open > thm \ < close > , \ < open > prop \ < close > and \ < open > term \ < close > admit an extra \ < ^ emph > \ < open > style \ < close > specification to modify the printed result . A style is specified by a name with a possibly empty number of arguments ; multiple styles can be sequenced with commas . The following standard styles are available : \ < ^ descr > \ < open > lhs \ < close > 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 . \ < ^ descr > \ < open > rhs \ < close > is like \ < open > lhs \ < close > , but extracts the second argument . \ < ^ descr > \ < open > concl \ < close > extracts the conclusion \ < open > C \ < close > from a rule in Horn - clause normal form \ < open > A \ < ^ sub > 1 \ < Longrightarrow > \ < dots > A \ < ^ sub > n \ < Longrightarrow > C \ < close > . \ < ^ descr > \ < open > prem \ < close > \ < open > n \ < close > extract premise number \ < open > n \ < close > from from a rule in Horn - clause normal form \ < open > A \ < ^ sub > 1 \ < Longrightarrow > \ < dots > A \ < ^ sub > n \ < Longrightarrow > C \ < close > . \ < close > subsection \ < open > General options \ < close > text \ < open > The following options are available to tune the printed output of antiquotations . Note that many of these coincide with system and configuration options of the same names . \ < ^ descr > @ { antiquotation_option_def show_types } ~ \ < open > = bool \ < close > and @ { antiquotation_option_def show_sorts } ~ \ < open > = bool \ < close > control printing of explicit type and sort constraints . \ < ^ descr > @ { antiquotation_option_def show_structs } ~ \ < open > = bool \ < close > controls printing of implicit structures . \ < ^ descr > @ { antiquotation_option_def show_abbrevs } ~ \ < open > = bool \ < close > controls folding of abbreviations . \ < ^ descr > @ { antiquotation_option_def names_long } ~ \ < open > = bool \ < close > forces names of types and constants etc . \ to be printed in their fully qualified internal form . \ < ^ descr > @ { antiquotation_option_def names_short } ~ \ < open > = bool \ < close > 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 . \ < ^ descr > @ { antiquotation_option_def names_unique } ~ \ < open > = bool \ < close > determines whether the printed version of qualified names should be made sufficiently long to avoid overlap with names declared further back . Set to \ < open > false \ < close > for more concise output . \ < ^ descr > @ { antiquotation_option_def eta_contract } ~ \ < open > = bool \ < close > prints terms in \ < open > \ < eta > \ < close > - contracted form . \ < ^ descr > @ { antiquotation_option_def display } ~ \ < open > = bool \ < close > 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 . \ < ^ descr > @ { antiquotation_option_def break } ~ \ < open > = bool \ < close > controls line breaks in non - display material . \ < ^ descr > @ { antiquotation_option_def cartouche } ~ \ < open > = bool \ < close > indicates if the output should be delimited as cartouche . \ < ^ descr > @ { antiquotation_option_def quotes } ~ \ < open > = bool \ < close > indicates if the output should be delimited via double quotes ( option @ { antiquotation_option cartouche } takes precedence ) . Note that the Isabelle { \ LaTeX } styles may suppress quotes on their own account . \ < ^ descr > @ { antiquotation_option_def mode } ~ \ < open > = name \ < close > adds \ < open > name \ < close > to the print mode to be used for presentation . Note that the standard setup for { \ LaTeX } output is already present by default , with mode ` ` \ < open > latex \ < close > ' ' . \ < ^ descr > @ { antiquotation_option_def margin } ~ \ < open > = nat \ < close > and @ { antiquotation_option_def indent } ~ \ < open > = nat \ < close > change the margin or indentation for pretty printing of display material . \ < ^ descr > @ { antiquotation_option_def goals_limit } ~ \ < open > = nat \ < close > determines the maximum number of subgoals to be printed ( for goal - based antiquotation ) . \ < ^ descr > @ { antiquotation_option_def source } ~ \ < open > = bool \ < close > 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 \ < open > term \ < close > and \ < open > typ \ < close > antiquotations with \ < open > source = false \ < close > involve a full round - trip from the original source to an internalized logical entity back to a source form , according to the syntax of the current context . Thus the printed output is not under direct control of the author , it may even fluctuate a bit as the underlying theory is changed later on . In contrast , @ { antiquotation_option source } ~ \ < open > = true \ < close > admits direct printing of the given source text , with the desirable well - formedness check in the background , but without modification of the printed text . Cartouche delimiters of the argument are stripped for antiquotations that are internally categorized as ` ` embedded ' ' . \ < ^ descr > @ { antiquotation_option_def source_cartouche } is like @ { antiquotation_option source } , but cartouche delimiters are always preserved in the output . For Boolean flags , ` ` \ < open > name = true \ < close > ' ' may be abbreviated as ` ` \ < open > name \ < close > ' ' . All of the above flags are disabled by default , unless changed specifically for a logic session in the corresponding \ < ^ verbatim > \ < open > ROOT \ < close > file . \ < close > section \ < open > Markdown - like text structure \ < close > text \ < open > The markup commands @ { command_ref text } , @ { command_ref txt } , @ { command_ref text_raw } ( \ secref { sec : markup } ) consist of plain text . Its internal structure consists of paragraphs and ( nested ) lists , using special Isabelle symbols and some rules for indentation and blank lines . This quasi - visual format resembles \ < ^ emph > \ < open > Markdown \ < close > \ < ^ footnote > \ < open > \ < ^ url > \ < open > http : / / commonmark . org \ < close > \ < close > , but the full complexity of that notation is avoided . This is a summary of the main principles of minimal Markdown in Isabelle : \ < ^ item > List items start with the following markers \ < ^ descr > [ itemize : ] \ < ^ verbatim > \ < open > \ < ^ item > \ < close > \ < ^ descr > [ enumerate : ] \ < ^ verbatim > \ < open > \ < ^ enum > \ < close > \ < ^ descr > [ description : ] \ < ^ verbatim > \ < open > \ < ^ descr > \ < close > \ < ^ item > Adjacent list items with same indentation and same marker are grouped into a single list . \ < ^ item > Singleton blank lines separate paragraphs . \ < ^ item > Multiple blank lines escape from the current list hierarchy . Notable differences to official Markdown : \ < ^ item > Indentation of list items needs to match exactly . \ < ^ item > Indentation is unlimited ( official Markdown interprets four spaces as block quote ) . \ < ^ item > List items always consist of paragraphs - - - there is no notion of ` ` tight ' ' list . \ < ^ item > Section headings are expressed via Isar document markup commands ( \ secref { sec : markup } ) . \ < ^ item > URLs , font styles , other special content is expressed via antiquotations ( \ secref { sec : antiq } ) , usually with proper nesting of sub - languages via text cartouches . \ < close > section \ < open > Document markers and command tags \ label { sec : document - markers } \ < close > text \ < open > \ emph { Document markers } are formal comments of the form \ < open > \ < ^ marker > \ < open > marker_body \ < close > \ < close > ( using the control symbol \ < ^ verbatim > \ < open > \ < ^ marker > \ < close > ) and may occur anywhere within the outer syntax of a command : the inner syntax of a marker body resembles that for attributes ( \ secref { sec : syn - att } ) . In contrast , \ emph { Command tags } may only occur after a command keyword and are treated as special markers as explained below . \ < ^ rail > \ < open > @ { syntax_def marker } : ' \ < ^ marker > ' @ { syntax cartouche } ; @ { syntax_def marker_body } : ( @ { syntax name } @ { syntax args } * ' , ' ) ; @ { syntax_def tags } : tag * ; tag : ' % ' ( @ { syntax short_ident } | @ { syntax string } ) \ < close > Document markers are stripped from the document output , but surrounding white - space is preserved : e . g . \ a marker at the end of a line does not affect the subsequent line break . Markers operate within the semantic presentation context of a command , and may modify it to change the overall appearance of a command span ( e . g . \ by adding tags ) . Each document marker has its own syntax defined in the theory context ; the following markers are predefined in Isabelle / Pure : \ < ^ rail > \ < open > ( @ @ { document_marker_def title } | @ @ { document_marker_def creator } | @ @ { document_marker_def contributor } | @ @ { document_marker_def date } | @ @ { document_marker_def license } | @ @ { document_marker_def description } ) @ { syntax embedded } ; @ @ { document_marker_def tag } ( scope ? ) @ { syntax name } ; scope : ' ( ' ( ' proof ' | ' command ' ) ' ) ' \ < close > \ < ^ descr > \ < open > \ < ^ marker > \ < open > title arg \ < close > \ < close > , \ < open > \ < ^ marker > \ < open > creator arg \ < close > \ < close > , \ < open > \ < ^ marker > \ < open > contributor arg \ < close > \ < close > , \ < open > \ < ^ marker > \ < open > date arg \ < close > \ < close > , \ < open > \ < ^ marker > \ < open > license arg \ < close > \ < close > , and \ < open > \ < ^ marker > \ < open > description arg \ < close > \ < close > produce markup in the PIDE document , without any immediate effect on typesetting . This vocabulary is taken from the Dublin Core Metadata Initiative \ < ^ footnote > \ < open > \ < ^ url > \ < open > https : / / www . dublincore . org / specifications / dublin - core / dcmi - terms \ < close > \ < close > . The argument is an uninterpreted string , except for @ { document_marker description } , which consists of words that are subject to spell - checking . \ < ^ descr > \ < open > \ < ^ marker > \ < open > tag name \ < close > \ < close > updates the list of command tags in the presentation context : later declarations take precedence , so \ < open > \ < ^ marker > \ < open > tag a , tag b , tag c \ < close > \ < close > produces a reversed list . The default tags are given by the original \ < ^ theory_text > \ < open > keywords \ < close > declaration of a command , and the system option @ { system_option_ref document_tags } . The optional \ < open > scope \ < close > tells how far the tagging is applied to subsequent proof structure : ` ` \ < ^ theory_text > \ < open > ( " proof " ) \ < close > ' ' means it applies to the following proof text , and ` ` \ < ^ theory_text > \ < open > ( command ) \ < close > ' ' means it only applies to the current command . The default within a proof body is ` ` \ < ^ theory_text > \ < open > ( " proof " ) \ < close > ' ' , but for toplevel goal statements it is ` ` \ < ^ theory_text > \ < open > ( command ) \ < close > ' ' . Thus a \ < open > tag \ < close > marker for \ < ^ theory_text > \ < open > theorem \ < close > , \ < ^ theory_text > \ < open > lemma \ < close > etc . does \ emph { not } affect its proof by default . An old - style command tag \ < ^ verbatim > \ < open > % \ < close > \ < open > name \ < close > is treated like a document marker \ < open > \ < ^ marker > \ < open > tag ( proof ) name \ < close > \ < close > : the list of command tags precedes the list of document markers . The head of the resulting tags in the presentation context is turned into { \ LaTeX } environments to modify the type - setting . The following tags are pre - declared for certain classes of commands , and serve as default markup for certain kinds of commands : \ < ^ medskip > \ begin { tabular } { ll } \ < open > document \ < close > & document markup commands \ \ \ < open > theory \ < close > & theory begin / end \ \ \ < open > proof \ < close > & all proof commands \ \ \ < open > ML \ < close > & all commands involving ML code \ \ \ end { tabular } \ < ^ medskip > The Isabelle document preparation system \ < ^ cite > \ < open > " isabelle - system " \ < close > allows tagged command regions to be presented specifically , e . g . \ to fold proof texts , or drop parts of the text completely . For example ` ` \ < ^ theory_text > \ < open > by auto \ < close > ~ \ < open > \ < ^ marker > \ < open > tag invisible \ < close > \ < close > ' ' causes that piece of proof to be treated as \ < open > invisible \ < close > instead of \ < open > proof \ < close > ( the default ) , which may be shown or hidden depending on the document setup . In contrast , ` ` \ < ^ theory_text > \ < open > by auto \ < close > ~ \ < open > \ < ^ marker > \ < open > tag visible \ < close > \ < close > ' ' forces this text to be shown invariably . Explicit tag specifications within a proof apply to all subsequent commands of the same level of nesting . For example , ` ` \ < ^ theory_text > \ < open > proof \ < close > ~ \ < open > \ < ^ marker > \ < open > tag invisible \ < close > \ < dots > \ < close > ~ \ < ^ theory_text > \ < open > qed \ < close > ' ' forces the whole sub - proof to be typeset as \ < open > visible \ < close > ( unless some of its parts are tagged differently ) . \ < ^ medskip > Command tags merely produce certain markup environments for type - setting . The meaning of these is determined by { \ LaTeX } macros , as defined in \ < ^ file > \ < open > ~ ~ / lib / texinputs / isabelle . sty \ < close > or by the document author . The Isabelle document preparation tools also provide some high - level options to specify the meaning of arbitrary tags to ` ` keep ' ' , ` ` drop ' ' , or ` ` fold ' ' the corresponding parts of the text . Logic sessions may also specify ` ` document versions ' ' , where given tags are interpreted in some particular way . Again see \ < ^ cite > \ < open > " isabelle - system " \ < close > for further details . \ < close > section \ < open > Railroad diagrams \ < close > text \ < open > \ begin { matharray } { rcl } @ { antiquotation_def " rail " } & : & \ < open > antiquotation \ < close > \ \ \ end { matharray } \ < ^ rail > \ < open > ' rail ' @ { syntax text } \ < close > The @ { antiquotation rail } antiquotation allows to include syntax diagrams into Isabelle documents . { \ LaTeX } requires the style file \ < ^ file > \ < open > ~ ~ / lib / texinputs / railsetup . sty \ < close > , which can be used via \ < ^ verbatim > \ < open > \ usepackage { railsetup } \ < close > in \ < ^ verbatim > \ < open > root . tex \ < close > , for example . The rail specification language is quoted here as Isabelle @ { syntax string } or text @ { syntax " cartouche " } ; it has its own grammar given below . \ begingroup \ def \ isasymnewline { \ isatt { \ isacharbackslash \ isacharless newline \ isachargreater } } \ < ^ rail > \ < open > rule ? + ' ; ' ; rule : ( ( identifier | @ { syntax antiquotation } ) ' : ' ) ? body ; body : concatenation + ' | ' ; concatenation : ( ( atom ' ? ' ? ) + ) ( ( ' * ' | ' + ' ) atom ? ) ? ; atom : ' ( ' body ? ' ) ' | identifier | ' @ ' ? ( string | @ { syntax antiquotation } ) | ' \ < newline > ' \ < close > \ endgroup The lexical syntax of \ < open > identifier \ < close > coincides with that of @ { syntax short_ident } in regular Isabelle syntax , but \ < open > string \ < close > uses single quotes instead of double quotes of the standard @ { syntax string } category . Each \ < open > rule \ < close > defines a formal language ( with optional name ) , using a notation that is similar to EBNF or regular expressions with recursion . The meaning and visual appearance of these rail language elements is illustrated by the following representative examples . \ < ^ item > Empty \ < ^ verbatim > \ < open > ( ) \ < close > \ < ^ rail > \ < open > ( ) \ < close > \ < ^ item > Nonterminal \ < ^ verbatim > \ < open > A \ < close > \ < ^ rail > \ < open > A \ < close > \ < ^ item > Nonterminal via Isabelle antiquotation \ < ^ verbatim > \ < open > @ { syntax method } \ < close > \ < ^ rail > \ < open > @ { syntax method } \ < close > \ < ^ item > Terminal \ < ^ verbatim > \ < open > ' xyz ' \ < close > \ < ^ rail > \ < open > ' xyz ' \ < close > \ < ^ item > Terminal in keyword style \ < ^ verbatim > \ < open > @ ' xyz ' \ < close > \ < ^ rail > \ < open > @ ' xyz ' \ < close > \ < ^ item > Terminal via Isabelle antiquotation \ < ^ verbatim > \ < open > @ @ { method rule } \ < close > \ < ^ rail > \ < open > @ @ { method rule } \ < close > \ < ^ item > Concatenation \ < ^ verbatim > \ < open > A B C \ < close > \ < ^ rail > \ < open > A B C \ < close > \ < ^ item > Newline inside concatenation \ < ^ verbatim > \ < open > A B C \ < newline > D E F \ < close > \ < ^ rail > \ < open > A B C \ < newline > D E F \ < close > \ < ^ item > Variants \ < ^ verbatim > \ < open > A | B | C \ < close > \ < ^ rail > \ < open > A | B | C \ < close > \ < ^ item > Option \ < ^ verbatim > \ < open > A ? \ < close > \ < ^ rail > \ < open > A ? \ < close > \ < ^ item > Repetition \ < ^ verbatim > \ < open > A * \ < close > \ < ^ rail > \ < open > A * \ < close > \ < ^ item > Repetition with separator \ < ^ verbatim > \ < open > A * sep \ < close > \ < ^ rail > \ < open > A * sep \ < close > \ < ^ item > Strict repetition \ < ^ verbatim > \ < open > A + \ < close > \ < ^ rail > \ < open > A + \ < close > \ < ^ item > Strict repetition with separator \ < ^ verbatim > \ < open > A + sep \ < close > \ < ^ rail > \ < open > A + sep \ < close > \ < close > end
Messung V0.5 in Prozent C=89 H=96 G=92
¤ Dauer der Verarbeitung: 0.47 Sekunden
¤ *© Formatika GbR, Deutschland
