# HG changeset patch # User wenzelm # Date 1445000006 -7200 # Node ID 987533262fc26558eb95c6218bfd04123f949837 # Parent 3e21699bb83bf53ed85b1e42d3dec85603206883 Markdown support in document text; diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Eq.thy --- a/src/Doc/Implementation/Eq.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Eq.thy Fri Oct 16 14:53:26 2015 +0200 @@ -98,8 +98,6 @@ @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole theorem by the given rules. @@ -119,8 +117,6 @@ "rules"}, re-ordered to fold longer expression first. This supports to idea to fold primitive definitions that appear in expended form in the proof state. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Integration.thy Fri Oct 16 14:53:26 2015 +0200 @@ -44,8 +44,6 @@ @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Toplevel.state} represents Isar toplevel states, which are normally manipulated through the concept of toplevel transitions only (\secref{sec:toplevel-transition}). @@ -63,8 +61,6 @@ \<^descr> @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof state if available, otherwise it raises an error. - - \end{description} \ text %mlantiq \ @@ -72,15 +68,11 @@ @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\ \end{matharray} - \begin{description} - \<^descr> @{text "@{Isar.state}"} refers to Isar toplevel state at that point --- as abstract value. This only works for diagnostic ML commands, such as @{command ML_val} or @{command ML_command}. - - \end{description} \ @@ -121,8 +113,6 @@ Toplevel.transition -> Toplevel.transition"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic function. @@ -146,8 +136,6 @@ \<^descr> @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding proof command, that returns the resulting theory, after applying the resulting facts to the target context. - - \end{description} \ text %mlex \The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example @@ -175,8 +163,6 @@ @{index_ML Thy_Info.register_thy: "theory -> unit"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML use_thy}~@{text A} ensures that theory @{text A} is fully up-to-date wrt.\ the external file store; outdated ancestors are reloaded on demand. @@ -199,8 +185,6 @@ \<^descr> @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing theory value with the theory loader database and updates source version information according to the file store. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Isar.thy --- a/src/Doc/Implementation/Isar.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Isar.thy Fri Oct 16 14:53:26 2015 +0200 @@ -8,8 +8,6 @@ @{cite \\S2\ "isabelle-isar-ref"}) consists of three main categories of language elements: - \begin{enumerate} - \<^enum> Proof \emph{commands} define the primary language of transactions of the underlying Isar/VM interpreter. Typical examples are @{command "fix"}, @{command "assume"}, @{command @@ -34,8 +32,6 @@ Typical examples are @{attribute intro} (which affects the context), and @{attribute symmetric} (which affects the theorem). - - \end{enumerate} \ @@ -79,8 +75,6 @@ (term * term list) list list -> Proof.context -> Proof.state"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Proof.state} represents Isar proof states. This is a block-structured configuration with proof context, linguistic mode, and optional goal. The latter consists of goal @@ -138,8 +132,6 @@ Isar source language. The original nested list structure over terms is turned into one over theorems when @{text "after_qed"} is invoked. - - \end{description} \ @@ -148,16 +140,12 @@ @{ML_antiquotation_def "Isar.goal"} & : & @{text ML_antiquotation} \\ \end{matharray} - \begin{description} - \<^descr> @{text "@{Isar.goal}"} refers to the regular goal state (if available) of the current proof state managed by the Isar toplevel --- as abstract value. This only works for diagnostic ML commands, such as @{command ML_val} or @{command ML_command}. - - \end{description} \ text %mlex \The following example peeks at a certain goal configuration.\ @@ -189,8 +177,6 @@ tactics need to hold for methods accordingly, with the following additions. - \begin{itemize} - \<^item> Goal addressing is further limited either to operate uniformly on \emph{all} subgoals, or specifically on the \emph{first} subgoal. @@ -211,7 +197,6 @@ is no sensible use of facts outside the goal state, facts should be inserted into the subgoals that are addressed by the method. - \end{itemize} \<^medskip> Syntactically, the language of proof methods appears as @@ -265,8 +250,6 @@ Empirically, any Isar proof method can be categorized as follows. - \begin{enumerate} - \<^enum> \emph{Special method with cases} with named context additions associated with the follow-up goal state. @@ -294,7 +277,6 @@ Example: @{method "rule_tac"}. - \end{enumerate} When implementing proof methods, it is advisable to study existing implementations carefully and imitate the typical ``boiler plate'' @@ -318,8 +300,6 @@ string -> theory -> theory"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Proof.method} represents proof methods as abstract type. @@ -349,8 +329,6 @@ \<^descr> @{ML Method.setup}~@{text "name parser description"} provides the functionality of the Isar command @{command method_setup} as ML function. - - \end{description} \ text %mlex \See also @{command method_setup} in @@ -546,8 +524,6 @@ string -> theory -> theory"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type attribute} represents attributes as concrete type alias. @@ -561,8 +537,6 @@ \<^descr> @{ML Attrib.setup}~@{text "name parser description"} provides the functionality of the Isar command @{command attribute_setup} as ML function. - - \end{description} \ text %mlantiq \ @@ -574,16 +548,12 @@ @@{ML_antiquotation attributes} attributes \} - \begin{description} - \<^descr> @{text "@{attributes [\]}"} embeds attribute source representation into the ML text, which is particularly useful with declarations like @{ML Local_Theory.note}. Attribute names are internalized at compile time, but the source is unevaluated. This means attributes with formal arguments (types, terms, theorems) may be subject to odd effects of dynamic scoping! - - \end{description} \ text %mlex \See also @{command attribute_setup} in diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Local_Theory.thy --- a/src/Doc/Implementation/Local_Theory.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Local_Theory.thy Fri Oct 16 14:53:26 2015 +0200 @@ -103,8 +103,6 @@ local_theory -> (string * thm list) * local_theory"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type local_theory} represents local theories. Although this is merely an alias for @{ML_type Proof.context}, it is semantically a subtype of the same: a @{ML_type local_theory} holds @@ -149,8 +147,6 @@ This is essentially the internal version of the @{command lemmas} command, or @{command declare} if an empty name binding is given. - - \end{description} \ diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Fri Oct 16 14:53:26 2015 +0200 @@ -138,8 +138,6 @@ @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type class} represents type classes. \<^descr> Type @{ML_type sort} represents sorts, i.e.\ finite @@ -185,8 +183,6 @@ \<^descr> @{ML Sign.primitive_arity}~@{text "(\, \<^vec>s, s)"} declares the arity @{text "\ :: (\<^vec>s)s"}. - - \end{description} \ text %mlantiq \ @@ -211,8 +207,6 @@ @@{ML_antiquotation typ} type \} - \begin{description} - \<^descr> @{text "@{class c}"} inlines the internalized class @{text "c"} --- as @{ML_type string} literal. @@ -231,8 +225,6 @@ \<^descr> @{text "@{typ \}"} inlines the internalized type @{text "\"} --- as constructor term for datatype @{ML_type typ}. - - \end{description} \ @@ -383,8 +375,6 @@ @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type term} represents de-Bruijn terms, with comments in abstractions, and explicitly named free variables and constants; this is a datatype with constructors @{index_ML Bound}, @{index_ML @@ -440,8 +430,6 @@ Sign.const_instance}~@{text "thy (c, [\\<^sub>1, \, \\<^sub>n])"} convert between two representations of polymorphic constants: full type instance vs.\ compact type arguments form. - - \end{description} \ text %mlantiq \ @@ -464,8 +452,6 @@ @@{ML_antiquotation prop} prop \} - \begin{description} - \<^descr> @{text "@{const_name c}"} inlines the internalized logical constant name @{text "c"} --- as @{ML_type string} literal. @@ -483,8 +469,6 @@ \<^descr> @{text "@{prop \}"} inlines the internalized proposition @{text "\"} --- as constructor term for datatype @{ML_type term}. - - \end{description} \ @@ -681,8 +665,6 @@ Defs.entry -> Defs.entry list -> theory -> theory"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Thm.peek_status}~@{text "thm"} informs about the current status of the derivation object behind the given theorem. This is a snapshot of a potentially ongoing (parallel) evaluation of proofs. @@ -778,8 +760,6 @@ declares dependencies of a named specification for constant @{text "c\<^sub>\"}, relative to existing specifications for constants @{text "\<^vec>d\<^sub>\"}. This also works for type constructors. - - \end{description} \ @@ -808,8 +788,6 @@ @'by' method method? \} - \begin{description} - \<^descr> @{text "@{ctyp \}"} produces a certified type wrt.\ the current background theory --- as abstract value of type @{ML_type ctyp}. @@ -840,9 +818,6 @@ "by"} step. More complex Isar proofs should be done in regular theory source, before compiling the corresponding ML text that uses the result. - - \end{description} - \ @@ -915,8 +890,6 @@ @{index_ML Logic.dest_type: "term -> typ"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text "A"} and @{text "B"}. @@ -933,8 +906,6 @@ \<^descr> @{ML Logic.dest_type}~@{text "TYPE(\)"} recovers the type @{text "\"}. - - \end{description} \ @@ -972,16 +943,12 @@ @{index_ML Thm.strip_shyps: "thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous sort hypotheses of the given theorem, i.e.\ the sorts that are not present within type variables of the statement. \<^descr> @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous sort hypotheses that can be witnessed from the type signature. - - \end{description} \ text %mlex \The following artificial example demonstrates the @@ -1069,8 +1036,6 @@ Regular user-level inferences in Isabelle/Pure always maintain the following canonical form of results: - \begin{itemize} - \<^item> Normalization by @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}, which is a theorem of Pure, means that quantifiers are pushed in front of implication at each level of nesting. The normal form is a @@ -1081,8 +1046,6 @@ \ A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \ A ?\<^vec>x"}. Note that this representation looses information about the order of parameters, and vacuous quantifiers vanish automatically. - - \end{itemize} \ text %mlref \ @@ -1090,14 +1053,10 @@ @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given theorem according to the canonical form specified above. This is occasionally helpful to repair some low-level tools that do not handle Hereditary Harrop Formulae properly. - - \end{description} \ @@ -1174,8 +1133,6 @@ @{index_ML_op "OF": "thm * thm list -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"}, according to the @{inference resolution} principle explained above. @@ -1211,8 +1168,6 @@ This corresponds to the rule attribute @{attribute OF} in Isar source language. - - \end{description} \ @@ -1359,8 +1314,6 @@ @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type proof} represents proof terms; this is a datatype with constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound}, @@ -1417,8 +1370,6 @@ \<^descr> @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"} pretty-prints the given proof term. - - \end{description} \ text %mlex \Detailed proof information of a theorem may be retrieved diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/ML.thy Fri Oct 16 14:53:26 2015 +0200 @@ -76,8 +76,8 @@ subsubsections, paragraphs etc.\ using a simple layout via ML comments as follows. - \begin{verbatim} - (*** section ***) + @{verbatim [display] +\ (*** section ***) (** subsection **) @@ -88,8 +88,7 @@ (* long paragraph, with more text - *) - \end{verbatim} + *)\} As in regular typography, there is some extra space \emph{before} section headings that are adjacent to plain text, but not other headings @@ -155,8 +154,8 @@ Example: - \begin{verbatim} - (* RIGHT *) + @{verbatim [display] +\ (* RIGHT *) fun print_foo ctxt foo = let @@ -180,15 +179,12 @@ fun print_foo ctxt foo = let fun aux t = ... string_of_term ctxt t ... - in ... end; - \end{verbatim} + in ... end;\} \paragraph{Specific conventions.} Here are some specific name forms that occur frequently in the sources. - \begin{itemize} - \<^item> A function that maps @{ML_text foo} to @{ML_text bar} is called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never @{ML_text foo2bar}, nor @{ML_text bar_from_foo}, nor @{ML_text @@ -212,17 +208,17 @@ \begin{itemize} - \<^item> theories are called @{ML_text thy}, rarely @{ML_text theory} - (never @{ML_text thry}) - - \<^item> proof contexts are called @{ML_text ctxt}, rarely @{ML_text - context} (never @{ML_text ctx}) - - \<^item> generic contexts are called @{ML_text context} - - \<^item> local theories are called @{ML_text lthy}, except for local - theories that are treated as proof context (which is a semantic - super-type) + \item theories are called @{ML_text thy}, rarely @{ML_text theory} + (never @{ML_text thry}) + + \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text + context} (never @{ML_text ctx}) + + \item generic contexts are called @{ML_text context} + + \item local theories are called @{ML_text lthy}, except for local + theories that are treated as proof context (which is a semantic + super-type) \end{itemize} @@ -237,21 +233,21 @@ \begin{itemize} - \<^item> sorts are called @{ML_text S} - - \<^item> types are called @{ML_text T}, @{ML_text U}, or @{ML_text - ty} (never @{ML_text t}) - - \<^item> terms are called @{ML_text t}, @{ML_text u}, or @{ML_text - tm} (never @{ML_text trm}) - - \<^item> certified types are called @{ML_text cT}, rarely @{ML_text - T}, with variants as for types - - \<^item> certified terms are called @{ML_text ct}, rarely @{ML_text - t}, with variants as for terms (never @{ML_text ctrm}) - - \<^item> theorems are called @{ML_text th}, or @{ML_text thm} + \item sorts are called @{ML_text S} + + \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text + ty} (never @{ML_text t}) + + \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text + tm} (never @{ML_text trm}) + + \item certified types are called @{ML_text cT}, rarely @{ML_text + T}, with variants as for types + + \item certified terms are called @{ML_text ct}, rarely @{ML_text + t}, with variants as for terms (never @{ML_text ctrm}) + + \item theorems are called @{ML_text th}, or @{ML_text thm} \end{itemize} @@ -269,9 +265,7 @@ before the latter two, and the general context is given first. Example: - \begin{verbatim} - fun my_tac ctxt arg1 arg2 i st = ... - \end{verbatim} + @{verbatim [display] \ fun my_tac ctxt arg1 arg2 i st = ...\} Note that the goal state @{ML_text st} above is rarely made explicit, if tactic combinators (tacticals) are used as usual. @@ -280,8 +274,6 @@ in the @{verbatim ctxt} argument above. Do not refer to the background theory of @{verbatim st} -- it is not a proper context, but merely a formal certificate. - - \end{itemize} \ @@ -307,16 +299,16 @@ defines positioning of spaces for parentheses, punctuation, and infixes as illustrated here: - \begin{verbatim} - val x = y + z * (a + b); + @{verbatim [display] +\ val x = y + z * (a + b); val pair = (a, b); - val record = {foo = 1, bar = 2}; - \end{verbatim} + val record = {foo = 1, bar = 2};\} Lines are normally broken \emph{after} an infix operator or punctuation character. For example: - \begin{verbatim} + @{verbatim [display] +\ val x = a + b + @@ -326,7 +318,7 @@ (a, b, c); - \end{verbatim} +\} Some special infixes (e.g.\ @{ML_text "|>"}) work better at the start of the line, but punctuation is always at the end. @@ -354,8 +346,8 @@ nesting depth, not the accidental length of the text that initiates a level of nesting. Example: - \begin{verbatim} - (* RIGHT *) + @{verbatim [display] +\ (* RIGHT *) if b then expr1_part1 @@ -370,8 +362,7 @@ if b then expr1_part1 expr1_part2 else expr2_part1 - expr2_part2 - \end{verbatim} + expr2_part2\} The second form has many problems: it assumes a fixed-width font when viewing the sources, it uses more space on the line and thus @@ -395,8 +386,8 @@ @{ML_text case} get extra indentation to indicate the nesting clearly. Example: - \begin{verbatim} - (* RIGHT *) + @{verbatim [display] +\ (* RIGHT *) fun foo p1 = expr1 @@ -409,16 +400,15 @@ fun foo p1 = expr1 | foo p2 = - expr2 - \end{verbatim} + expr2\} Body expressions consisting of @{ML_text case} or @{ML_text let} require care to maintain compositionality, to prevent loss of logical indentation where it is especially important to see the structure of the text. Example: - \begin{verbatim} - (* RIGHT *) + @{verbatim [display] +\ (* RIGHT *) fun foo p1 = (case e of @@ -442,8 +432,7 @@ ... in ... - end - \end{verbatim} + end\} Extra parentheses around @{ML_text case} expressions are optional, but help to analyse the nesting based on character matching in the @@ -453,41 +442,36 @@ There are two main exceptions to the overall principle of compositionality in the layout of complex expressions. - \begin{enumerate} - \<^enum> @{ML_text "if"} expressions are iterated as if ML had multi-branch conditionals, e.g. - \begin{verbatim} - (* RIGHT *) + @{verbatim [display] +\ (* RIGHT *) if b1 then e1 else if b2 then e2 - else e3 - \end{verbatim} + else e3\} \<^enum> @{ML_text fn} abstractions are often layed-out as if they would lack any structure by themselves. This traditional form is motivated by the possibility to shift function arguments back and forth wrt.\ additional combinators. Example: - \begin{verbatim} - (* RIGHT *) + @{verbatim [display] +\ (* RIGHT *) fun foo x y = fold (fn z => - expr) - \end{verbatim} + expr)\} Here the visual appearance is that of three arguments @{ML_text x}, @{ML_text y}, @{ML_text z} in a row. - \end{enumerate} Such weakly structured layout should be use with great care. Here are some counter-examples involving @{ML_text let} expressions: - \begin{verbatim} - (* WRONG *) + @{verbatim [display] +\ (* WRONG *) fun foo x = let val y = ... @@ -515,8 +499,7 @@ let val y = ... in - ... end - \end{verbatim} + ... end\} \<^medskip> In general the source layout is meant to emphasize the @@ -646,8 +629,6 @@ @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of the ML toplevel --- at compile time. ML code needs to take care to refer to @{ML "ML_Context.the_generic_context ()"} @@ -664,7 +645,6 @@ \<^descr> @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a singleton fact. - \end{description} It is important to note that the above functions are really restricted to the compile time, even though the ML compiler is @@ -725,8 +705,6 @@ @@{ML_antiquotation print} @{syntax name}? \} - \begin{description} - \<^descr> @{text "@{make_string}"} inlines a function to print arbitrary values similar to the ML toplevel. The result is compiler dependent and may fall back on "?" in certain situations. The value of configuration option @@ -736,8 +714,6 @@ unit"} to output the result of @{text "@{make_string}"} above, together with the source position of the antiquotation. The default output function is @{ML writeln}. - - \end{description} \ text %mlex \The following artificial examples show how to produce @@ -907,8 +883,6 @@ @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML fold}~@{text f} lifts the parametrized update function @{text "f"} to a list of parameters. @@ -919,7 +893,6 @@ function @{text "f"} (with side-result) to a list of parameters and cumulative side-results. - \end{description} \begin{warn} The literature on functional programming provides a confusing multitude of @@ -1033,8 +1006,6 @@ @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\ \end{mldecls} - \begin{description} - \<^descr> @{ML writeln}~@{text "text"} outputs @{text "text"} as regular message. This is the primary message output operation of Isabelle and should be used by default. @@ -1068,7 +1039,6 @@ this is normally not used directly in user code. \end{warn} - \end{description} \begin{warn} Regular Isabelle/ML code should output messages exclusively by the @@ -1215,8 +1185,6 @@ @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML try}~@{text "f x"} makes the partiality of evaluating @{text "f x"} explicit via the option datatype. Interrupts are \emph{not} handled here, i.e.\ this form serves as safe replacement @@ -1247,8 +1215,6 @@ Inserting @{ML Runtime.exn_trace} into ML code temporarily is useful for debugging, but not suitable for production code. - - \end{description} \ text %mlantiq \ @@ -1256,14 +1222,10 @@ @{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\ \end{matharray} - \begin{description} - \<^descr> @{text "@{assert}"} inlines a function @{ML_type "bool -> unit"} that raises @{ML Fail} if the argument is @{ML false}. Due to inlining the source position of failed assertions is included in the error output. - - \end{description} \ @@ -1276,8 +1238,6 @@ in itself a small string, which has either one of the following forms: - \begin{enumerate} - \<^enum> a single ASCII character ``@{text "c"}'', for example ``@{verbatim a}'', @@ -1298,7 +1258,6 @@ "<^raw"}@{text n}@{verbatim ">"}, where @{text n} consists of digits, for example ``@{verbatim "\<^raw42>"}''. - \end{enumerate} The @{text "ident"} syntax for symbol names is @{text "letter (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and @{text @@ -1337,8 +1296,6 @@ @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type "Symbol.symbol"} represents individual Isabelle symbols. @@ -1363,7 +1320,6 @@ \<^descr> @{ML "Symbol.decode"} converts the string representation of a symbol into the datatype version. - \end{description} \paragraph{Historical note.} In the original SML90 standard the primitive ML type @{ML_type char} did not exists, and @{ML_text @@ -1399,13 +1355,9 @@ @{index_ML_type char} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type char} is \emph{not} used. The smallest textual unit in Isabelle is represented as a ``symbol'' (see \secref{sec:symbols}). - - \end{description} \ @@ -1416,8 +1368,6 @@ @{index_ML_type string} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type string} represents immutable vectors of 8-bit characters. There are operations in SML to convert back and forth to actual byte vectors, which are seldom used. @@ -1428,20 +1378,18 @@ \begin{enumerate} - \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), - with @{ML Symbol.explode} as key operation; - - \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), - with @{ML YXML.parse_body} as key operation. - + \item sequence of Isabelle symbols (see also \secref{sec:symbols}), + with @{ML Symbol.explode} as key operation; + + \item XML tree structure via YXML (see also @{cite "isabelle-system"}), + with @{ML YXML.parse_body} as key operation. + \end{enumerate} Note that Isabelle/ML string literals may refer Isabelle symbols like ``@{verbatim \}'' natively, \emph{without} escaping the backslash. This is a consequence of Isabelle treating all source text as strings of symbols, instead of raw characters. - - \end{description} \ text %mlex \The subsequent example illustrates the difference of @@ -1471,8 +1419,6 @@ @{index_ML_type int} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type int} represents regular mathematical integers, which are \emph{unbounded}. Overflow is treated properly, but should never happen in practice.\footnote{The size limit for integer bit patterns in memory is @@ -1486,8 +1432,6 @@ @{ML_structure Int}. Structure @{ML_structure Integer} in @{file "~~/src/Pure/General/integer.ML"} provides some additional operations. - - \end{description} \ @@ -1499,8 +1443,6 @@ @{index_ML seconds: "real -> Time.time"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Time.time} represents time abstractly according to the SML97 basis library definition. This is adequate for internal ML operations, but awkward in concrete time specifications. @@ -1510,8 +1452,6 @@ point numbers are easy to use as configuration options in the context (see \secref{sec:config-options}) or system options that are maintained externally. - - \end{description} \ @@ -1551,8 +1491,6 @@ @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML cons}~@{text "x xs"} evaluates to @{text "x :: xs"}. Tupled infix operators are a historical accident in Standard ML. @@ -1571,8 +1509,6 @@ often more appropriate in declarations of context data (\secref{sec:context-data}) that are issued by the user in Isar source: later declarations take precedence over earlier ones. - - \end{description} \ text %mlex \Using canonical @{ML fold} together with @{ML cons} (or @@ -1627,8 +1563,6 @@ @{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML AList.lookup}, @{ML AList.defined}, @{ML AList.update} implement the main ``framework operations'' for mappings in Isabelle/ML, following standard conventions for their names and @@ -1644,7 +1578,6 @@ justify its independent existence. This also gives the implementation some opportunity for peep-hole optimization. - \end{description} Association lists are adequate as simple implementation of finite mappings in many practical situations. A more advanced table structure is defined in @@ -1762,8 +1695,6 @@ read/write access to shared resources, which are outside the purely functional world of ML. This covers the following in particular. - \begin{itemize} - \<^item> Global references (or arrays), i.e.\ mutable memory cells that persist over several invocations of associated operations.\footnote{This is independent of the visibility of such @@ -1775,7 +1706,6 @@ \<^item> Writable resources in the file-system that are shared among different threads or external processes. - \end{itemize} Isabelle/ML provides various mechanisms to avoid critical shared resources in most situations. As last resort there are some @@ -1783,8 +1713,6 @@ help to make Isabelle/ML programs work smoothly in a concurrent environment. - \begin{itemize} - \<^item> Avoid global references altogether. Isabelle/Isar maintains a uniform context that incorporates arbitrary data declared by user programs (\secref{sec:context-data}). This context is passed as @@ -1824,8 +1752,6 @@ serial numbers in Isabelle/ML. Thus temporary files that are passed to to some external process will be always disjoint, and thus thread-safe. - - \end{itemize} \ text %mlref \ @@ -1834,16 +1760,12 @@ @{index_ML serial_string: "unit -> string"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML File.tmp_path}~@{text "path"} relocates the base component of @{text "path"} into the unique temporary directory of the running Isabelle/ML process. \<^descr> @{ML serial_string}~@{text "()"} creates a new serial number that is unique over the runtime of the Isabelle/ML process. - - \end{description} \ text %mlex \The following example shows how to create unique @@ -1881,8 +1803,6 @@ ('a -> ('b * 'a) option) -> 'b"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type "'a Synchronized.var"} represents synchronized variables with state of type @{ML_type 'a}. @@ -1900,7 +1820,6 @@ signal to all waiting threads on the associated condition variable, and returns the result @{text "y"}. - \end{description} There are some further variants of the @{ML Synchronized.guarded_access} combinator, see @{file @@ -1994,8 +1913,6 @@ @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type "'a Exn.result"} represents the disjoint sum of ML results explicitly, with constructor @{ML Exn.Res} for regular values and @{ML "Exn.Exn"} for exceptions. @@ -2026,8 +1943,6 @@ occurred in the original evaluation process is raised again, the others are ignored. That single exception may get handled by conventional means in ML. - - \end{description} \ @@ -2055,8 +1970,6 @@ @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Par_List.map}~@{text "f [x\<^sub>1, \, x\<^sub>n]"} is like @{ML "map"}~@{text "f [x\<^sub>1, \, x\<^sub>n]"}, but the evaluation of @{text "f x\<^sub>i"} for @{text "i = 1, \, n"} is performed in parallel. @@ -2078,8 +1991,6 @@ This generic parallel choice combinator is the basis for derived forms, such as @{ML Par_List.find_some}, @{ML Par_List.exists}, @{ML Par_List.forall}. - - \end{description} \ text %mlex \Subsequently, the Ackermann function is evaluated in @@ -2128,8 +2039,6 @@ @{index_ML Lazy.force: "'a lazy -> 'a"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type @{verbatim "'a"}. @@ -2145,8 +2054,6 @@ \<^descr> @{ML Lazy.force}~@{text x} produces the result of the lazy value in a thread-safe manner as explained above. Thus it may cause the current thread to wait on a pending evaluation attempt by another thread. - - \end{description} \ @@ -2221,8 +2128,6 @@ @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type "'a future"} represents future values over type @{verbatim "'a"}. @@ -2237,39 +2142,39 @@ \begin{itemize} - \<^item> @{text "name : string"} (default @{ML "\"\""}) specifies a common name - for the tasks of the forked futures, which serves diagnostic purposes. - - \<^item> @{text "group : Future.group option"} (default @{ML NONE}) specifies - an optional task group for the forked futures. @{ML NONE} means that a new - sub-group of the current worker-thread task context is created. If this is - not a worker thread, the group will be a new root in the group hierarchy. - - \<^item> @{text "deps : Future.task list"} (default @{ML "[]"}) specifies - dependencies on other future tasks, i.e.\ the adjacency relation in the - global task queue. Dependencies on already finished tasks are ignored. - - \<^item> @{text "pri : int"} (default @{ML 0}) specifies a priority within the - task queue. - - Typically there is only little deviation from the default priority @{ML 0}. - As a rule of thumb, @{ML "~1"} means ``low priority" and @{ML 1} means - ``high priority''. - - Note that the task priority only affects the position in the queue, not the - thread priority. When a worker thread picks up a task for processing, it - runs with the normal thread priority to the end (or until canceled). Higher - priority tasks that are queued later need to wait until this (or another) - worker thread becomes free again. - - \<^item> @{text "interrupts : bool"} (default @{ML true}) tells whether the - worker thread that processes the corresponding task is initially put into - interruptible state. This state may change again while running, by modifying - the thread attributes. - - With interrupts disabled, a running future task cannot be canceled. It is - the responsibility of the programmer that this special state is retained - only briefly. + \item @{text "name : string"} (default @{ML "\"\""}) specifies a common name + for the tasks of the forked futures, which serves diagnostic purposes. + + \item @{text "group : Future.group option"} (default @{ML NONE}) specifies + an optional task group for the forked futures. @{ML NONE} means that a new + sub-group of the current worker-thread task context is created. If this is + not a worker thread, the group will be a new root in the group hierarchy. + + \item @{text "deps : Future.task list"} (default @{ML "[]"}) specifies + dependencies on other future tasks, i.e.\ the adjacency relation in the + global task queue. Dependencies on already finished tasks are ignored. + + \item @{text "pri : int"} (default @{ML 0}) specifies a priority within the + task queue. + + Typically there is only little deviation from the default priority @{ML 0}. + As a rule of thumb, @{ML "~1"} means ``low priority" and @{ML 1} means + ``high priority''. + + Note that the task priority only affects the position in the queue, not the + thread priority. When a worker thread picks up a task for processing, it + runs with the normal thread priority to the end (or until canceled). Higher + priority tasks that are queued later need to wait until this (or another) + worker thread becomes free again. + + \item @{text "interrupts : bool"} (default @{ML true}) tells whether the + worker thread that processes the corresponding task is initially put into + interruptible state. This state may change again while running, by modifying + the thread attributes. + + With interrupts disabled, a running future task cannot be canceled. It is + the responsibility of the programmer that this special state is retained + only briefly. \end{itemize} @@ -2336,8 +2241,6 @@ \<^descr> @{ML Future.fulfill}~@{text "x a"} finishes the passive future @{text x} by the given value @{text a}. If the promise has already been canceled, the attempt to fulfill it causes an exception. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Prelim.thy Fri Oct 16 14:53:26 2015 +0200 @@ -26,8 +26,6 @@ Contexts and derivations are linked by the following key principles: - \begin{itemize} - \<^item> Transfer: monotonicity of derivations admits results to be transferred into a \emph{larger} context, i.e.\ @{text "\ \\<^sub>\ \"} implies @{text "\' \\<^sub>\\<^sub>' \"} for contexts @{text "\' @@ -39,7 +37,6 @@ @{text "\ = \' - \"}. Note that @{text "\"} remains unchanged here, only the @{text "\"} part is affected. - \end{itemize} \<^medskip> By modeling the main characteristics of the primitive @@ -129,8 +126,6 @@ @{index_ML Theory.ancestors_of: "theory -> theory list"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type theory} represents theory contexts. \<^descr> @{ML "Context.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict @@ -151,8 +146,6 @@ \<^descr> @{ML "Theory.ancestors_of"}~@{text "thy"} returns all ancestors of @{text thy} (not including @{text thy} itself). - - \end{description} \ text %mlantiq \ @@ -167,8 +160,6 @@ @@{ML_antiquotation theory_context} nameref \} - \begin{description} - \<^descr> @{text "@{theory}"} refers to the background theory of the current context --- as abstract value. @@ -179,8 +170,6 @@ \<^descr> @{text "@{theory_context A}"} is similar to @{text "@{theory A}"}, but presents the result as initial @{ML_type Proof.context} (see also @{ML Proof_Context.init_global}). - - \end{description} \ @@ -220,8 +209,6 @@ @{index_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Proof.context} represents proof contexts. \<^descr> @{ML Proof_Context.init_global}~@{text "thy"} produces a proof @@ -233,8 +220,6 @@ \<^descr> @{ML Proof_Context.transfer}~@{text "thy ctxt"} promotes the background theory of @{text "ctxt"} to the super theory @{text "thy"}. - - \end{description} \ text %mlantiq \ @@ -242,16 +227,12 @@ @{ML_antiquotation_def "context"} & : & @{text ML_antiquotation} \\ \end{matharray} - \begin{description} - \<^descr> @{text "@{context}"} refers to \emph{the} context at compile-time --- as abstract value. Independently of (local) theory or proof mode, this always produces a meaningful result. This is probably the most common antiquotation in interactive experimentation with ML inside Isar. - - \end{description} \ @@ -279,8 +260,6 @@ @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Context.generic} is the direct sum of @{ML_type "theory"} and @{ML_type "Proof.context"}, with the datatype constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}. @@ -293,8 +272,6 @@ proof context from the generic @{text "context"}, using @{ML "Proof_Context.init_global"} as required (note that this re-initializes the context data with each invocation). - - \end{description} \ @@ -383,8 +360,6 @@ @{index_ML_functor Generic_Data} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML_functor Theory_Data}@{text "(spec)"} declares data for type @{ML_type theory} according to the specification provided as argument structure. The resulting structure provides data init and @@ -395,8 +370,6 @@ \<^descr> @{ML_functor Generic_Data}@{text "(spec)"} is analogous to @{ML_functor Theory_Data} for type @{ML_type Context.generic}. - - \end{description} \ text %mlex \ @@ -456,7 +429,6 @@ \<^medskip> Our intended invariant is achieved as follows: - \begin{enumerate} \<^enum> @{ML Wellformed_Terms.add} only admits terms that have passed the @{ML Sign.cert_term} check of the given theory at that point. @@ -466,7 +438,6 @@ upwards in the hierarchy (via extension or merges), and maintain wellformedness without further checks. - \end{enumerate} Note that all basic operations of the inference kernel (which includes @{ML Sign.cert_term}) observe this monotonicity principle, @@ -544,8 +515,6 @@ string Config.T"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Config.get}~@{text "ctxt config"} gets the value of @{text "config"} in the given context. @@ -563,8 +532,6 @@ \<^descr> @{ML Attrib.config_int}, @{ML Attrib.config_real}, and @{ML Attrib.config_string} work like @{ML Attrib.config_bool}, but for types @{ML_type int} and @{ML_type string}, respectively. - - \end{description} \ text %mlex \The following example shows how to declare and use a @@ -621,7 +588,6 @@ Subsequently, we shall introduce specific categories of names. Roughly speaking these correspond to logical entities as follows: - \begin{itemize} \<^item> Basic names (\secref{sec:basic-name}): free and bound variables. @@ -632,8 +598,6 @@ (type constructors, term constants, other concepts defined in user space). Such entities are typically managed via name spaces (\secref{sec:name-space}). - - \end{itemize} \ @@ -690,8 +654,6 @@ @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Name.internal}~@{text "name"} produces an internal name by adding one underscore. @@ -718,8 +680,6 @@ Variable}, which is also able to provide an official status of ``locally fixed variable'' within the logical environment (cf.\ \secref{sec:variables}). - - \end{description} \ text %mlex \The following simple examples demonstrate how to produce @@ -775,15 +735,12 @@ Isabelle syntax observes the following rules for representing an indexname @{text "(x, i)"} as a packed string: - \begin{itemize} - \<^item> @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"}, \<^item> @{text "?xi"} if @{text "x"} does not end with a digit, \<^item> @{text "?x.i"} otherwise. - \end{itemize} Indexnames may acquire large index numbers after several maxidx shifts have been applied. Results are usually normalized towards @@ -798,15 +755,11 @@ @{index_ML_type indexname: "string * int"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type indexname} represents indexed names. This is an abbreviation for @{ML_type "string * int"}. The second component is usually non-negative, except for situations where @{text "(x, -1)"} is used to inject basic names into this type. Other negative indexes should not be used. - - \end{description} \ @@ -843,8 +796,6 @@ @{index_ML Long_Name.explode: "string -> string list"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Long_Name.base_name}~@{text "name"} returns the base name of a long name. @@ -857,8 +808,6 @@ \<^descr> @{ML Long_Name.implode}~@{text "names"} and @{ML Long_Name.explode}~@{text "name"} convert between the packed string representation and the explicit list form of long names. - - \end{description} \ @@ -947,8 +896,6 @@ @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"} \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type binding} represents the abstract concept of name bindings. @@ -1026,8 +973,6 @@ \<^descr> @{ML Name_Space.is_concealed}~@{text "space name"} indicates whether @{text "name"} refers to a strictly private entity that other tools are supposed to ignore! - - \end{description} \ text %mlantiq \ @@ -1039,14 +984,10 @@ @@{ML_antiquotation binding} name \} - \begin{description} - \<^descr> @{text "@{binding name}"} produces a binding with base name @{text "name"} and the source position taken from the concrete syntax of this antiquotation. In many situations this is more appropriate than the more basic @{ML Binding.name} function. - - \end{description} \ text %mlex \The following example yields the source position of some diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Proof.thy Fri Oct 16 14:53:26 2015 +0200 @@ -114,8 +114,6 @@ ((string * (string * typ)) list * term) * Proof.context"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term variables @{text "xs"}, returning the resulting internal names. By default, the internal representation coincides with the external @@ -156,8 +154,6 @@ \<^descr> @{ML Variable.focus}~@{text "bindings B"} decomposes the outermost @{text "\"} prefix of proposition @{text "B"}, using the given name bindings. - - \end{description} \ text %mlex \The following example shows how to work with fixed term @@ -291,8 +287,6 @@ @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type Assumption.export} represents arbitrary export rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"}, where the @{ML_type "bool"} indicates goal mode, @@ -319,8 +313,6 @@ this is a goal context. The result is in HHF normal form. Note that @{ML "Proof_Context.export"} combines @{ML "Variable.export"} and @{ML "Assumption.export"} in the canonical way. - - \end{description} \ text %mlex \The following example demonstrates how rules can be @@ -419,8 +411,6 @@ Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure of the specified sub-goal, producing an extended context and a reduced goal, which needs to be solved by the given tactic. All @@ -466,8 +456,6 @@ given facts using a tactic, which results in additional fixed variables and assumptions in the context. Final results need to be exported explicitly. - - \end{description} \ text %mlex \The following minimal example illustrates how to access diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Syntax.thy --- a/src/Doc/Implementation/Syntax.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Syntax.thy Fri Oct 16 14:53:26 2015 +0200 @@ -36,13 +36,10 @@ \secref{sec:term-check}, respectively. This results in the following decomposition of the main operations: - \begin{itemize} - \<^item> @{text "read = parse; check"} \<^item> @{text "pretty = uncheck; unparse"} - \end{itemize} For example, some specification package might thus intercept syntax processing at a well-defined stage after @{text "parse"}, to a augment the @@ -88,8 +85,6 @@ @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a simultaneous list of source strings as types of the logic. @@ -128,7 +123,6 @@ be concatenated with other strings, as long as there is no further formatting and line-breaking involved. - \end{description} @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML Syntax.string_of_term} are the most important operations in practice. @@ -179,8 +173,6 @@ @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as pre-type that is ready to be used with subsequent check operations. @@ -200,7 +192,6 @@ uncheck operations, to turn it into a pretty tree. There is no distinction for propositions here. - \end{description} These operations always operate on a single item; use the combinator @{ML map} to apply them to a list. @@ -247,8 +238,6 @@ @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list of pre-types as types of the logic. Typically, this involves normalization of type synonyms. @@ -276,7 +265,6 @@ list of terms of the logic, in preparation of pretty printing. There is no distinction for propositions here. - \end{description} These operations always operate simultaneously on a list; use the combinator @{ML singleton} to apply them to a single item. diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Tactic.thy Fri Oct 16 14:53:26 2015 +0200 @@ -70,8 +70,6 @@ @{index_ML Goal.conclude: "thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML "Goal.init"}~@{text C} initializes a tactical goal from the well-formed proposition @{text C}. @@ -86,8 +84,6 @@ \<^descr> @{ML "Goal.conclude"}~@{text "thm"} removes the goal protection, even if there are pending subgoals. - - \end{description} \ @@ -150,8 +146,6 @@ The main well-formedness conditions for proper tactics are summarized as follows. - \begin{itemize} - \<^item> General tactic failure is indicated by an empty result, only serious faults may produce an exception. @@ -164,7 +158,6 @@ \<^item> Range errors in subgoal addressing produce an empty result. - \end{itemize} Some of these conditions are checked by higher-level goal infrastructure (\secref{sec:struct-goals}); others are not checked @@ -187,8 +180,6 @@ @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type tactic} represents tactics. The well-formedness conditions described above need to be observed. See also @{file "~~/src/Pure/General/seq.ML"} for the underlying @@ -233,8 +224,6 @@ \<^descr> @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put @{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but without changing the main goal protection. - - \end{description} \ @@ -264,8 +253,6 @@ sequence enumerates all possibilities of the following choices (if applicable): - \begin{enumerate} - \<^enum> selecting one of the rules given as argument to the tactic; \<^enum> selecting a subgoal premise to eliminate, unifying it against @@ -274,7 +261,6 @@ \<^enum> unifying the conclusion of the subgoal to the conclusion of the rule. - \end{enumerate} Recall that higher-order unification may produce multiple results that are enumerated here. @@ -295,8 +281,6 @@ @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state using the given theorems, which should normally be introduction rules. The tactic resolves a rule's conclusion with subgoal @{text @@ -350,7 +334,6 @@ These tactics were written for a specific application within the classical reasoner. Flexible subgoals are not updated at will, but are left alone. - \end{description} \ @@ -419,8 +402,6 @@ @{index_ML rename_tac: "string list -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the rule @{text thm} with the instantiations @{text insts}, as described above, and then performs resolution on subgoal @{text i}. @@ -449,7 +430,6 @@ parameters of subgoal @{text i} according to the provided @{text names} (which need to be distinct identifiers). - \end{description} For historical reasons, the above instantiation tactics take unparsed string arguments, which makes them hard to use in general @@ -473,8 +453,6 @@ @{index_ML flexflex_tac: "Proof.context -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal @{text i} by @{text n} positions: from right to left if @{text n} is positive, and from left to right if @{text n} is negative. @@ -491,8 +469,6 @@ unification. To prevent this, use @{ML Rule_Insts.res_inst_tac} to instantiate some variables in a rule. Normally flex-flex constraints can be ignored; they often disappear as unknowns get instantiated. - - \end{description} \ @@ -513,8 +489,6 @@ @{index_ML_op COMP: "thm * thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal @{text "i"} using @{text "rule"}, without lifting. The @{text "rule"} is taken to have the form @{text "\\<^sub>1 \ \ \\<^sub>m \ \"}, where @@ -534,7 +508,6 @@ \<^descr> @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose (thm\<^sub>1, 1, thm\<^sub>2)"}. - \end{description} \begin{warn} These low-level operations are stepping outside the structure @@ -581,8 +554,6 @@ @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal state, it returns all states reachable in two steps by applying @@ -621,8 +592,6 @@ "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}. The other primed tacticals work analogously. - - \end{description} \ @@ -641,8 +610,6 @@ @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal state and returns the resulting sequence, if non-empty; otherwise it returns the original state. Thus, it applies @{text "tac"} at most @@ -672,15 +639,11 @@ \<^descr> @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound by @{text "n"} (where @{ML "~1"} means @{text "\"}). - - \end{description} \ text %mlex \The basic tactics and tacticals considered above follow some algebraic laws: - \begin{itemize} - \<^item> @{ML all_tac} is the identity element of the tactical @{ML_op "THEN"}. @@ -692,8 +655,6 @@ \<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) functions over more basic combinators (ignoring some internal implementation tricks): - - \end{itemize} \ ML \ @@ -747,8 +708,6 @@ @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac n"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{text "tac 1"}. It applies the @{text tac} to all the subgoals, counting downwards. @@ -774,8 +733,6 @@ @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the corresponding range of subgoals, counting downwards. - - \end{description} \ @@ -800,8 +757,6 @@ @{index_ML CHANGED: "tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the goal state and returns a sequence consisting of those result goal states that are satisfactory in the sense of @{text "sat"}. @@ -810,8 +765,6 @@ state and returns precisely those states that differ from the original state (according to @{ML Thm.eq_thm}). Thus @{ML CHANGED}~@{text "tac"} always has some effect on the state. - - \end{description} \ @@ -824,8 +777,6 @@ @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if @{text "sat"} returns true. Otherwise it applies @{text "tac"}, then recursively searches from each element of the resulting @@ -839,8 +790,6 @@ \<^descr> @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to search for states having fewer subgoals than the given state. Thus, it insists upon solving at least one subgoal. - - \end{description} \ @@ -857,8 +806,6 @@ However, they do not enumerate all solutions; they terminate after the first satisfactory result from @{text "tac"}. - \begin{description} - \<^descr> @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first search to find states for which @{text "sat"} is true. For most applications, it is too slow. @@ -880,8 +827,6 @@ the result of applying @{text "tac\<^sub>0"} to the goal state. This tactical permits separate tactics for starting the search and continuing the search. - - \end{description} \ @@ -895,8 +840,6 @@ @{index_ML DETERM: "tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to the goal state if it satisfies predicate @{text "sat"}, and applies @{text "tac\<^sub>2"}. It is a conditional tactical in that only one of @@ -915,8 +858,6 @@ \<^descr> @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal state and returns the head of the resulting sequence. @{ML DETERM} limits the search space by making its argument deterministic. - - \end{description} \ @@ -930,8 +871,6 @@ @{index_ML size_of_thm: "thm -> int"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text "thm"} has fewer than @{text "n"} premises. @@ -948,8 +887,6 @@ "thm"}, namely the number of variables, constants and abstractions in its conclusion. It may serve as a distance function for @{ML BEST_FIRST}. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Oct 16 14:53:26 2015 +0200 @@ -49,8 +49,6 @@ @@{command text_raw} @{syntax text} \} - \begin{description} - \<^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 @@ -68,7 +66,6 @@ manipulations becomes available, at the risk of messing up document output. - \end{description} Except for @{command "text_raw"}, the text passed to any of the above markup commands may refer to formal entities via \emph{document @@ -187,8 +184,6 @@ comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} nor verbatim text @{verbatim "{*"}~@{text "\"}~@{verbatim "*}"}. - \begin{description} - \<^descr> @{command "print_antiquotations"} prints all document antiquotations that are defined in the current context; the ``@{text "!"}'' option indicates extra verbosity. @@ -290,8 +285,6 @@ @{antiquotation_option_def cite_macro}, or the configuration option @{attribute cite_macro} in the context. For example, @{text "@{cite [cite_macro = nocite] foobar}"} produces @{verbatim \\nocite{foobar}\}. - - \end{description} \ @@ -303,8 +296,6 @@ empty number of arguments; multiple styles can be sequenced with commas. The following standard styles are available: - \begin{description} - \<^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. @@ -318,8 +309,6 @@ \<^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"} - - \end{description} \ @@ -329,8 +318,6 @@ of antiquotations. Note that many of these coincide with system and configuration options of the same names. - \begin{description} - \<^descr> @{antiquotation_option_def show_types}~@{text "= bool"} and @{antiquotation_option_def show_sorts}~@{text "= bool"} control printing of explicit type and sort constraints. @@ -404,12 +391,12 @@ well-formedness check in the background, but without modification of the printed text. - \end{description} For Boolean flags, ``@{text "name = true"}'' may be abbreviated as ``@{text name}''. All of the above flags are disabled by default, unless changed specifically for a logic session in the corresponding - @{verbatim "ROOT"} file.\ + @{verbatim "ROOT"} file. +\ section \Markup via command tags \label{sec:tags}\ @@ -514,8 +501,6 @@ recursion. The meaning and visual appearance of these rail language elements is illustrated by the following representative examples. - \begin{itemize} - \<^item> Empty @{verbatim "()"} @{rail \()\} @@ -574,8 +559,6 @@ \<^item> Strict repetition with separator @{verbatim "A + sep"} @{rail \A + sep\} - - \end{itemize} \ @@ -590,14 +573,10 @@ @@{command display_drafts} (@{syntax name} +) \} - \begin{description} - \<^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. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Fri Oct 16 14:53:26 2015 +0200 @@ -38,8 +38,6 @@ @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))? \} - \begin{description} - \<^descr> @{command "print_options"} prints the available configuration options, with names, types, and current values; the ``@{text "!"}'' option indicates extra verbosity. @@ -48,8 +46,6 @@ named option, with the syntax of the value depending on the option's type. For @{ML_type bool} the default value is @{text true}. Any attempt to change a global option in a local context is ignored. - - \end{description} \ @@ -83,8 +79,6 @@ @@{method sleep} @{syntax real} \} - \begin{description} - \<^descr> @{method unfold}~@{text "a\<^sub>1 \ a\<^sub>n"} and @{method fold}~@{text "a\<^sub>1 \ a\<^sub>n"} expand (or fold back) the given definitions throughout all goals; any chained facts provided are inserted into the goal and @@ -129,7 +123,6 @@ s} seconds. This is occasionally useful for demonstration and testing purposes. - \end{description} \begin{matharray}{rcl} @{attribute_def tagged} & : & @{text attribute} \\ @@ -155,8 +148,6 @@ @@{attribute rotated} @{syntax int}? \} - \begin{description} - \<^descr> @{attribute tagged}~@{text "name value"} and @{attribute untagged}~@{text name} add and remove \emph{tags} of some theorem. Tags may be any list of string pairs that serve as formal comment. @@ -189,8 +180,6 @@ \<^descr> @{attribute no_vars} replaces schematic variables by free ones; this is mainly for tuning output of pretty printed theorems. - - \end{description} \ @@ -216,8 +205,6 @@ provide the canonical way for automated normalization (see \secref{sec:simplifier}). - \begin{description} - \<^descr> @{method subst}~@{text eq} performs a single substitution step using rule @{text eq}, which may be either a meta or object equality. @@ -257,8 +244,6 @@ Note that the @{method simp} method already involves repeated application of split rules as declared in the current context, using @{attribute split}, for example. - - \end{description} \ @@ -305,8 +290,6 @@ 'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs} \} - \begin{description} - \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after inserting chained facts as additional goal premises; further rule declarations may be included via @{text "(simp add: facts)"}. @@ -364,7 +347,6 @@ \<^descr> @{attribute simp_depth_limit} limits the number of recursive invocations of the Simplifier during conditional rewriting. - \end{description} By default the Simplifier methods above take local assumptions fully into account, using equational assumptions in the subsequent @@ -513,8 +495,6 @@ @@{command print_simpset} ('!'?) \} - \begin{description} - \<^descr> @{attribute simp} declares rewrite rules, by adding or deleting them from the simpset within the theory or proof context. Rewrite rules are theorems expressing some form of equality, for @@ -543,36 +523,36 @@ \begin{enumerate} - \<^enum> First-order patterns, considering the sublanguage of - application of constant operators to variable operands, without - @{text "\"}-abstractions or functional variables. - For example: + \item First-order patterns, considering the sublanguage of + application of constant operators to variable operands, without + @{text "\"}-abstractions or functional variables. + For example: - @{text "(?x + ?y) + ?z \ ?x + (?y + ?z)"} \\ - @{text "f (f ?x ?y) ?z \ f ?x (f ?y ?z)"} + @{text "(?x + ?y) + ?z \ ?x + (?y + ?z)"} \\ + @{text "f (f ?x ?y) ?z \ f ?x (f ?y ?z)"} - \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. - These are terms in @{text "\"}-normal form (this will always be the - case unless you have done something strange) where each occurrence - of an unknown is of the form @{text "?F x\<^sub>1 \ x\<^sub>n"}, where the - @{text "x\<^sub>i"} are distinct bound variables. + \item Higher-order patterns in the sense of @{cite "nipkow-patterns"}. + These are terms in @{text "\"}-normal form (this will always be the + case unless you have done something strange) where each occurrence + of an unknown is of the form @{text "?F x\<^sub>1 \ x\<^sub>n"}, where the + @{text "x\<^sub>i"} are distinct bound variables. - For example, @{text "(\x. ?P x \ ?Q x) \ (\x. ?P x) \ (\x. ?Q x)"} - or its symmetric form, since the @{text "rhs"} is also a - higher-order pattern. + For example, @{text "(\x. ?P x \ ?Q x) \ (\x. ?P x) \ (\x. ?Q x)"} + or its symmetric form, since the @{text "rhs"} is also a + higher-order pattern. - \<^enum> Physical first-order patterns over raw @{text "\"}-term - structure without @{text "\\\"}-equality; abstractions and bound - variables are treated like quasi-constant term material. + \item Physical first-order patterns over raw @{text "\"}-term + structure without @{text "\\\"}-equality; abstractions and bound + variables are treated like quasi-constant term material. - For example, the rule @{text "?f ?x \ range ?f = True"} rewrites the - term @{text "g a \ range g"} to @{text "True"}, but will fail to - match @{text "g (h b) \ range (\x. g (h x))"}. However, offending - subterms (in our case @{text "?f ?x"}, which is not a pattern) can - be replaced by adding new variables and conditions like this: @{text - "?y = ?f ?x \ ?y \ range ?f = True"} is acceptable as a conditional - rewrite rule of the second category since conditions can be - arbitrary terms. + For example, the rule @{text "?f ?x \ range ?f = True"} rewrites the + term @{text "g a \ range g"} to @{text "True"}, but will fail to + match @{text "g (h b) \ range (\x. g (h x))"}. However, offending + subterms (in our case @{text "?f ?x"}, which is not a pattern) can + be replaced by adding new variables and conditions like this: @{text + "?y = ?f ?x \ ?y \ range ?f = True"} is acceptable as a conditional + rewrite rule of the second category since conditions can be + arbitrary terms. \end{enumerate} @@ -634,7 +614,6 @@ simpset and the context of the problem being simplified may lead to unexpected results. - \end{description} The implicit simpset of the theory context is propagated monotonically through the theory hierarchy: forming a new theory, @@ -706,8 +685,6 @@ permutative.) When dealing with an AC-operator @{text "f"}, keep the following points in mind: - \begin{itemize} - \<^item> The associative law must always be oriented from left to right, namely @{text "f (f x y) z = f x (f y z)"}. The opposite orientation, if used with commutativity, leads to looping in @@ -717,7 +694,6 @@ associativity (A) and commutativity (C) but also a derived rule \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}. - \end{itemize} Ordered rewriting with the combination of A, C, and LC sorts a term lexicographically --- the rewriting engine imitates bubble-sort. @@ -794,8 +770,6 @@ These attributes and configurations options control various aspects of Simplifier tracing and debugging. - \begin{description} - \<^descr> @{attribute simp_trace} makes the Simplifier output internal operations. This includes rewrite steps, but also bookkeeping like modifications of the simpset. @@ -825,8 +799,6 @@ patterns which are checked for matches on the redex of a rule application. Theorem breakpoints trigger when the corresponding theorem is applied in a rewrite step. For example: - - \end{description} \ (*<*)experiment begin(*>*) @@ -866,8 +838,6 @@ @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+) \} - \begin{description} - \<^descr> @{command "simproc_setup"} defines a named simplification procedure that is invoked by the Simplifier whenever any of the given term patterns match the current redex. The implementation, @@ -891,8 +861,6 @@ add or delete named simprocs to the current Simplifier context. The default is to add a simproc. Note that @{command "simproc_setup"} already adds the new simproc to the subsequent context. - - \end{description} \ @@ -944,8 +912,6 @@ rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \ ?m < ?n"}, the default strategy could loop. % FIXME !?? - \begin{description} - \<^descr> @{ML Simplifier.set_subgoaler}~@{text "tac ctxt"} sets the subgoaler of the context to @{text "tac"}. The tactic will be applied to the context of the running Simplifier instance. @@ -955,7 +921,6 @@ the Simplifier has been told to utilize local assumptions in the first place (cf.\ the options in \secref{sec:simp-meth}). - \end{description} As an example, consider the following alternative subgoaler: \ @@ -1014,8 +979,6 @@ tactic is not totally safe: it may instantiate unknowns that appear also in other subgoals. - \begin{description} - \<^descr> @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text "tac"} into a solver; the @{text "name"} is only attached as a comment and has no further significance. @@ -1034,7 +997,6 @@ additional unsafe solver; it will be tried after the solvers which had already been present in @{text "ctxt"}. - \end{description} \<^medskip> The solver tactic is invoked with the context of the @@ -1100,8 +1062,6 @@ conditional. Another possibility is to apply an elimination rule on the assumptions. More adventurous loopers could start an induction. - \begin{description} - \<^descr> @{text "ctxt setloop tac"} installs @{text "tac"} as the only looper tactic of @{text "ctxt"}. @@ -1121,7 +1081,6 @@ tactic corresponding to @{text thm} from the looper tactics of @{text "ctxt"}. - \end{description} The splitter replaces applications of a given function; the right-hand side of the replacement can be anything. For example, @@ -1174,8 +1133,6 @@ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')' \} - \begin{description} - \<^descr> @{attribute simplified}~@{text "a\<^sub>1 \ a\<^sub>n"} causes a theorem to be simplified, either by exactly the specified rules @{text "a\<^sub>1, \, a\<^sub>n"}, or the implicit Simplifier context if no arguments are given. @@ -1188,8 +1145,6 @@ (\secref{sec:simp-strategies}) are \emph{not} involved here. The @{attribute simplified} attribute should be only rarely required under normal circumstances. - - \end{description} \ @@ -1436,8 +1391,6 @@ @@{attribute iff} (((() | 'add') '?'?) | 'del') \} - \begin{description} - \<^descr> @{command "print_claset"} prints the collection of rules declared to the Classical Reasoner, i.e.\ the @{ML_type claset} within the context. @@ -1487,8 +1440,6 @@ "\ P \ (\ R \ P) \ R"} in the second position. This is mainly for illustrative purposes: the Classical Reasoner already swaps rules internally as explained above. - - \end{description} \ @@ -1504,8 +1455,6 @@ @@{method rule} @{syntax thmrefs}? \} - \begin{description} - \<^descr> @{method rule} as offered by the Classical Reasoner is a refinement over the Pure one (see \secref{sec:pure-meth-att}). Both versions work the same, but the classical version observes the @@ -1520,8 +1469,6 @@ deriving any result from both @{text "\ A"} and @{text A}. Chained facts, which are guaranteed to participate, may appear in either order. - - \end{description} \ @@ -1564,8 +1511,6 @@ (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs} \} - \begin{description} - \<^descr> @{method blast} is a separate classical tableau prover that uses the same classical rule declarations as explained before. @@ -1576,23 +1521,23 @@ \begin{itemize} - \<^item> It does not use the classical wrapper tacticals, such as the - integration with the Simplifier of @{method fastforce}. + \item It does not use the classical wrapper tacticals, such as the + integration with the Simplifier of @{method fastforce}. - \<^item> It does not perform higher-order unification, as needed by the - rule @{thm [source=false] rangeI} in HOL. There are often - alternatives to such rules, for example @{thm [source=false] - range_eqI}. + \item It does not perform higher-order unification, as needed by the + rule @{thm [source=false] rangeI} in HOL. There are often + alternatives to such rules, for example @{thm [source=false] + range_eqI}. - \<^item> Function variables may only be applied to parameters of the - subgoal. (This restriction arises because the prover does not use - higher-order unification.) If other function variables are present - then the prover will fail with the message - @{verbatim [display] \Function unknown's argument not a bound variable\} + \item Function variables may only be applied to parameters of the + subgoal. (This restriction arises because the prover does not use + higher-order unification.) If other function variables are present + then the prover will fail with the message + @{verbatim [display] \Function unknown's argument not a bound variable\} - \<^item> Its proof strategy is more general than @{method fast} but can - be slower. If @{method blast} fails or seems to be running forever, - try @{method fast} and the other proof tools described below. + \item Its proof strategy is more general than @{method fast} but can + be slower. If @{method blast} fails or seems to be running forever, + try @{method fast} and the other proof tools described below. \end{itemize} @@ -1649,7 +1594,6 @@ slower, for example if the assumptions have many universal quantifiers. - \end{description} Any of the above methods support additional modifiers of the context of classical (and simplifier) rules, but the ones related to the @@ -1679,8 +1623,6 @@ @@{method clarsimp} (@{syntax clasimpmod} * ) \} - \begin{description} - \<^descr> @{method safe} repeatedly performs safe steps on all subgoals. It is deterministic, with at most one outcome. @@ -1690,8 +1632,6 @@ \<^descr> @{method clarsimp} acts like @{method clarify}, but also does simplification. Note that if the Simplifier context includes a splitter for the premises, the subgoal may still be split. - - \end{description} \ @@ -1710,8 +1650,6 @@ of the Classical Reasoner. By calling them yourself, you can execute these procedures one step at a time. - \begin{description} - \<^descr> @{method safe_step} performs a safe step on the first subgoal. The safe wrapper tacticals are applied to a tactic that may include proof by assumption or Modus Ponens (taking care not to instantiate @@ -1736,8 +1674,6 @@ Modus Ponens, etc., may be performed provided they do not instantiate unknowns. Assumptions of the form @{text "x = t"} may be eliminated. The safe wrapper tactical is applied. - - \end{description} \ @@ -1790,8 +1726,6 @@ wrapper names. These names may be used to selectively delete wrappers. - \begin{description} - \<^descr> @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper, which should yield a safe tactic, to modify the existing safe step tactic. @@ -1828,8 +1762,6 @@ \<^descr> @{text "addss"} adds the simpset of the context to its classical set. The assumptions and goal will be simplified, before the each unsafe step of the search. - - \end{description} \ @@ -1872,8 +1804,6 @@ @@{attribute rule_format} ('(' 'noasm' ')')? \} - \begin{description} - \<^descr> @{command "judgment"}~@{text "c :: \ (mx)"} declares constant @{text c} as the truth judgment of the current object-logic. Its type @{text \} should specify a coercion of the category of @@ -1908,8 +1838,6 @@ rule_format} is to replace (bounded) universal quantification (@{text "\"}) and implication (@{text "\"}) by the corresponding rule statements over @{text "\"} and @{text "\"}. - - \end{description} \ @@ -1928,8 +1856,6 @@ but sometimes needs extra care to identify problems. These tracing options may help. - \begin{description} - \<^descr> @{attribute unify_trace_simp} controls tracing of the simplification phase of higher-order unification. @@ -1949,7 +1875,6 @@ value in practice. If the search is cut off, unification prints a warning ``Unification bound exceeded''. - \end{description} \begin{warn} Options for unification cannot be modified in a local context. Only diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Oct 16 14:53:26 2015 +0200 @@ -116,8 +116,6 @@ @@{attribute (HOL) mono} (() | 'add' | 'del') \} - \begin{description} - \<^descr> @{command (HOL) "inductive"} and @{command (HOL) "coinductive"} define (co)inductive predicates from the introduction rules. @@ -150,8 +148,6 @@ \<^descr> @{attribute (HOL) mono} declares monotonicity rules in the context. These rule are involved in the automated monotonicity proof of the above inductive and coinductive definitions. - - \end{description} \ @@ -160,8 +156,6 @@ text \A (co)inductive definition of @{text R} provides the following main theorems: - \begin{description} - \<^descr> @{text R.intros} is the list of introduction rules as proven theorems, for the recursive predicates (or sets). The rules are also available individually, using the names given them in the @@ -175,7 +169,6 @@ \<^descr> @{text R.simps} is the equation unrolling the fixpoint of the predicate one step. - \end{description} When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are defined simultaneously, the list of introduction rules is called @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the @@ -192,8 +185,6 @@ sources for some examples. The general format of such monotonicity theorems is as follows: - \begin{itemize} - \<^item> Theorems of the form @{text "A \ B \ \ A \ \ B"}, for proving monotonicity of inductive definitions whose introduction rules have premises involving terms such as @{text "\ R t"}. @@ -218,8 +209,6 @@ @{prop "(P \ Q) \ \ P \ Q"} \qquad\qquad @{prop "Ball A P \ \x. x \ A \ P x"} \] - - \end{itemize} \ subsubsection \Examples\ @@ -290,8 +279,6 @@ @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and') \} - \begin{description} - \<^descr> @{command (HOL) "primrec"} defines primitive recursive functions over datatypes (see also @{command_ref (HOL) datatype}). The given @{text equations} specify reduction rules that are produced by instantiating the @@ -344,7 +331,6 @@ produces rules that eliminate the given equalities, following the cases given in the function definition. - \end{description} Recursive definitions introduced by the @{command (HOL) "function"} command accommodate reasoning by induction (cf.\ @{method induct}): rule @@ -360,8 +346,6 @@ The @{command (HOL) "function"} command accepts the following options. - \begin{description} - \<^descr> @{text sequential} enables a preprocessor which disambiguates overlapping patterns by making them mutually disjoint. Earlier equations take precedence over later ones. This allows to give the specification in @@ -374,8 +358,6 @@ \<^descr> @{text domintros} enables the automated generation of introduction rules for the domain predicate. While mostly not needed, they can be helpful in some proofs about partial functions. - - \end{description} \ @@ -535,8 +517,6 @@ orders: ( 'max' | 'min' | 'ms' ) * \} - \begin{description} - \<^descr> @{method (HOL) pat_completeness} is a specialized method to solve goals regarding the completeness of pattern matching, as required by the @{command (HOL) "function"} package (cf.\ @@ -576,8 +556,6 @@ patterns. This factors out some operations that are done internally by the function package and makes them available separately. See @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples. - - \end{description} \ @@ -594,8 +572,6 @@ @'where' @{syntax thmdecl}? @{syntax prop} \} - \begin{description} - \<^descr> @{command (HOL) "partial_function"}~@{text "(mode)"} defines recursive functions based on fixpoints in complete partial orders. No termination proof is required from the user or @@ -621,21 +597,21 @@ \begin{description} - \<^descr> @{text option} defines functions that map into the @{type - option} type. Here, the value @{term None} is used to model a - non-terminating computation. Monotonicity requires that if @{term - None} is returned by a recursive call, then the overall result must - also be @{term None}. This is best achieved through the use of the - monadic operator @{const "Option.bind"}. - - \<^descr> @{text tailrec} defines functions with an arbitrary result - type and uses the slightly degenerated partial order where @{term - "undefined"} is the bottom element. Now, monotonicity requires that - if @{term undefined} is returned by a recursive call, then the - overall result must also be @{term undefined}. In practice, this is - only satisfied when each recursive call is a tail call, whose result - is directly returned. Thus, this mode of operation allows the - definition of arbitrary tail-recursive functions. + \item @{text option} defines functions that map into the @{type + option} type. Here, the value @{term None} is used to model a + non-terminating computation. Monotonicity requires that if @{term + None} is returned by a recursive call, then the overall result must + also be @{term None}. This is best achieved through the use of the + monadic operator @{const "Option.bind"}. + + \item @{text tailrec} defines functions with an arbitrary result + type and uses the slightly degenerated partial order where @{term + "undefined"} is the bottom element. Now, monotonicity requires that + if @{term undefined} is returned by a recursive call, then the + overall result must also be @{term undefined}. In practice, this is + only satisfied when each recursive call is a tail call, whose result + is directly returned. Thus, this mode of operation allows the + definition of arbitrary tail-recursive functions. \end{description} @@ -645,8 +621,6 @@ \<^descr> @{attribute (HOL) partial_function_mono} declares rules for use in the internal monotonicity proofs of partial function definitions. - - \end{description} \ @@ -671,8 +645,6 @@ (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod} \} - \begin{description} - \<^descr> @{command (HOL) "recdef"} defines general well-founded recursive functions (using the TFL package), see also @{cite "isabelle-HOL"}. The ``@{text "(permissive)"}'' option tells @@ -684,7 +656,6 @@ (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\ \secref{sec:classical}). - \end{description} \<^medskip> Hints for @{command (HOL) "recdef"} may be also declared @@ -725,8 +696,6 @@ (@{syntax nameref} (@{syntax term} + ) + @'and') \} - \begin{description} - \<^descr> @{command "adhoc_overloading"}~@{text "c v\<^sub>1 ... v\<^sub>n"} associates variants with an existing constant. @@ -739,8 +708,6 @@ are printed instead of their respective overloaded constants. This is occasionally useful to check whether the system agrees with a user's expectations about derived variants. - - \end{description} \ @@ -758,8 +725,6 @@ decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')? \} - \begin{description} - \<^descr> @{command (HOL) "specification"}~@{text "decls \"} sets up a goal stating the existence of terms with the properties specified to hold for the constants given in @{text decls}. After finishing the @@ -771,8 +736,6 @@ specification given. The definition for the constant @{text c} is bound to the name @{text c_def} unless a theorem name is given in the declaration. Overloaded constants should be declared as such. - - \end{description} \ @@ -795,15 +758,12 @@ cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}? \} - \begin{description} - \<^descr> @{command (HOL) "old_datatype"} defines old-style inductive datatypes in HOL. \<^descr> @{command (HOL) "old_rep_datatype"} represents existing types as old-style datatypes. - \end{description} These commands are mostly obsolete; @{command (HOL) "datatype"} should be used instead. @@ -906,15 +866,12 @@ Two key observations make extensible records in a simply typed language like HOL work out: - \begin{enumerate} - \<^enum> the more part is internalized, as a free term or type variable, \<^enum> field names are externalized, they cannot be accessed within the logic as first-class values. - \end{enumerate} \<^medskip> In Isabelle/HOL record types have to be defined explicitly, @@ -943,8 +900,6 @@ constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}? \} - \begin{description} - \<^descr> @{command (HOL) "record"}~@{text "(\\<^sub>1, \, \\<^sub>m) t = \ + c\<^sub>1 :: \\<^sub>1 \ c\<^sub>n :: \\<^sub>n"} defines extensible record type @{text "(\\<^sub>1, \, \\<^sub>m) t"}, derived from the optional parent record @{text "\"} by adding new @@ -971,8 +926,6 @@ "(\\<^sub>1, \, \\<^sub>m, \) t_scheme"} made an abbreviation for @{text "\c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\"}. - - \end{description} \ @@ -1062,8 +1015,6 @@ reason about record structures quite conveniently. Assume that @{text t} is a record type as specified above. - \begin{enumerate} - \<^enum> Standard conversions for selectors or updates applied to record constructor terms are made part of the default Simplifier context; thus proofs by reduction of basic operations merely require the @{method simp} @@ -1098,8 +1049,6 @@ @{text "t.extend"}, @{text "t.truncate"} are \emph{not} treated automatically, but usually need to be expanded by hand, using the collective fact @{text "t.defs"}. - - \end{enumerate} \ @@ -1177,8 +1126,6 @@ dependent type: the meaning relies on the operations provided by different type-class instances. - \begin{description} - \<^descr> @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} defines a new type @{text "(\\<^sub>1, \, \\<^sub>n) t"} from the set @{text A} over an existing type. The set @{text A} may contain type variables @{text "\\<^sub>1, \, \\<^sub>n"} @@ -1223,8 +1170,6 @@ surjectivity. These rules are already declared as set or type rules for the generic @{method cases} and @{method induct} methods, respectively. - - \end{description} \ @@ -1272,8 +1217,6 @@ @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term} \} - \begin{description} - \<^descr> @{command (HOL) "functor"}~@{text "prefix: m"} allows to prove and register properties about the functorial structure of type constructors. These properties then can be used by other packages to deal with those @@ -1296,8 +1239,6 @@ theory and @{text "\\<^sub>1"}, \ldots, @{text "\\<^sub>k"} is a subsequence of @{text "\\<^sub>1 \ \\<^sub>1"}, @{text "\\<^sub>1 \ \\<^sub>1"}, \ldots, @{text "\\<^sub>n \ \\<^sub>n"}, @{text "\\<^sub>n \ \\<^sub>n"}. - - \end{description} \ @@ -1330,8 +1271,6 @@ quot_parametric: @'parametric' @{syntax thmref} \} - \begin{description} - \<^descr> @{command (HOL) "quotient_type"} defines a new quotient type @{text \}. The injection from a quotient type to a raw type is called @{text rep_\}, its inverse @{text abs_\} unless explicit @{keyword (HOL) @@ -1350,8 +1289,6 @@ extra argument of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}. This theorem allows the Lifting package to generate a stronger transfer rule for equality. - - \end{description} \ @@ -1405,33 +1342,31 @@ @{syntax thmref} (@{syntax thmref} @{syntax thmref})? \} - \begin{description} - \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with a user-defined type. The command supports two modes. \begin{enumerate} - \<^enum> The first one is a low-level mode when the user must provide as a - first argument of @{command (HOL) "setup_lifting"} a quotient theorem - @{term "Quotient R Abs Rep T"}. The package configures a transfer rule for - equality, a domain transfer rules and sets up the @{command_def (HOL) - "lift_definition"} command to work with the abstract type. An optional - theorem @{term "reflp R"}, which certifies that the equivalence relation R - is total, can be provided as a second argument. This allows the package to - generate stronger transfer rules. And finally, the parametricity theorem - for @{term R} can be provided as a third argument. This allows the package - to generate a stronger transfer rule for equality. - - Users generally will not prove the @{text Quotient} theorem manually for - new types, as special commands exist to automate the process. - - \<^enum> When a new subtype is defined by @{command (HOL) typedef}, @{command - (HOL) "lift_definition"} can be used in its second mode, where only the - @{term type_definition} theorem @{term "type_definition Rep Abs A"} is - used as an argument of the command. The command internally proves the - corresponding @{term Quotient} theorem and registers it with @{command - (HOL) setup_lifting} using its first mode. + \item The first one is a low-level mode when the user must provide as a + first argument of @{command (HOL) "setup_lifting"} a quotient theorem + @{term "Quotient R Abs Rep T"}. The package configures a transfer rule for + equality, a domain transfer rules and sets up the @{command_def (HOL) + "lift_definition"} command to work with the abstract type. An optional + theorem @{term "reflp R"}, which certifies that the equivalence relation R + is total, can be provided as a second argument. This allows the package to + generate stronger transfer rules. And finally, the parametricity theorem + for @{term R} can be provided as a third argument. This allows the package + to generate a stronger transfer rule for equality. + + Users generally will not prove the @{text Quotient} theorem manually for + new types, as special commands exist to automate the process. + + \item When a new subtype is defined by @{command (HOL) typedef}, @{command + (HOL) "lift_definition"} can be used in its second mode, where only the + @{term type_definition} theorem @{term "type_definition Rep Abs A"} is + used as an argument of the command. The command internally proves the + corresponding @{term Quotient} theorem and registers it with @{command + (HOL) setup_lifting} using its first mode. \end{enumerate} @@ -1490,16 +1425,16 @@ \begin{description} - \<^descr> @{text "\"} is a type variable - - \<^descr> @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, - where @{text "\"} is an abstract type constructor and @{text "\\<^sub>1 \ \\<^sub>n"} - do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas - @{typ "int dlist dlist"} not) - - \<^descr> @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, @{text "\"} is a type constructor that - was defined as a (co)datatype whose constructor argument types do not - contain either non-free datatypes or the function type. + \item @{text "\"} is a type variable + + \item @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, + where @{text "\"} is an abstract type constructor and @{text "\\<^sub>1 \ \\<^sub>n"} + do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas + @{typ "int dlist dlist"} not) + + \item @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, @{text "\"} is a type constructor that + was defined as a (co)datatype whose constructor argument types do not + contain either non-free datatypes or the function type. \end{description} @@ -1603,8 +1538,6 @@ "relator_distr"}. Also the definition of a relator and predicator is provided automatically. Moreover, if the BNF represents a datatype, simplification rules for a predicator are again proved automatically. - - \end{description} \ @@ -1628,8 +1561,6 @@ @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\ \end{matharray} - \begin{description} - \<^descr> @{method (HOL) "transfer"} method replaces the current subgoal with a logically equivalent one that uses different types and constants. The replacement of types and constants is guided by the database of transfer @@ -1712,7 +1643,6 @@ property is proved automatically if the involved type is BNF without dead variables. - \end{description} Theoretical background can be found in @{cite "Huffman-Kuncar:2013:lifting_transfer"}. @@ -1753,8 +1683,6 @@ @@{method (HOL) lifting_setup} @{syntax thmrefs}? \} - \begin{description} - \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the quotient type. @@ -1815,8 +1743,6 @@ the quotient extension theorem should be @{term "Quotient3 R Abs Rep \ Quotient3 (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems are stored in a database and are used all the steps of lifting theorems. - - \end{description} \ @@ -1855,8 +1781,6 @@ facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')' \} % FIXME check args "value" - \begin{description} - \<^descr> @{command (HOL) "solve_direct"} checks whether the current subgoals can be solved directly by an existing theorem. Duplicate lemmas can be detected in this way. @@ -1880,8 +1804,6 @@ \<^descr> @{command (HOL) "sledgehammer_params"} changes @{command (HOL) "sledgehammer"} configuration options persistently. - - \end{description} \ @@ -1929,8 +1851,6 @@ args: ( @{syntax name} '=' value + ',' ) \} % FIXME check "value" - \begin{description} - \<^descr> @{command (HOL) "value"}~@{text t} evaluates and prints a term; optionally @{text modes} can be specified, which are appended to the current print mode; see \secref{sec:print-modes}. @@ -1960,7 +1880,7 @@ \begin{description} - \<^descr>[@{text tester}] specifies which testing approach to apply. + \item[@{text tester}] specifies which testing approach to apply. There are three testers, @{text exhaustive}, @{text random}, and @{text narrowing}. An unknown configuration option is treated as an argument to tester, making @{text "tester ="} optional. When @@ -1971,31 +1891,31 @@ quickcheck_random_active}, @{attribute quickcheck_narrowing_active} are set to true. - \<^descr>[@{text size}] specifies the maximum size of the search space + \item[@{text size}] specifies the maximum size of the search space for assignment values. - \<^descr>[@{text genuine_only}] sets quickcheck only to return genuine + \item[@{text genuine_only}] sets quickcheck only to return genuine counterexample, but not potentially spurious counterexamples due to underspecified functions. - \<^descr>[@{text abort_potential}] sets quickcheck to abort once it + \item[@{text abort_potential}] sets quickcheck to abort once it found a potentially spurious counterexample and to not continue to search for a further genuine counterexample. For this option to be effective, the @{text genuine_only} option must be set to false. - \<^descr>[@{text eval}] takes a term or a list of terms and evaluates + \item[@{text eval}] takes a term or a list of terms and evaluates these terms under the variable assignment found by quickcheck. This option is currently only supported by the default (exhaustive) tester. - \<^descr>[@{text iterations}] sets how many sets of assignments are + \item[@{text iterations}] sets how many sets of assignments are generated for each particular size. - \<^descr>[@{text no_assms}] specifies whether assumptions in + \item[@{text no_assms}] specifies whether assumptions in structured proofs should be ignored. - \<^descr>[@{text locale}] specifies how to process conjectures in + \item[@{text locale}] specifies how to process conjectures in a locale context, i.e.\ they can be interpreted or expanded. The option is a whitespace-separated list of the two words @{text interpret} and @{text expand}. The list determines the @@ -2004,25 +1924,25 @@ The option is only provided as attribute declaration, but not as parameter to the command. - \<^descr>[@{text timeout}] sets the time limit in seconds. - - \<^descr>[@{text default_type}] sets the type(s) generally used to + \item[@{text timeout}] sets the time limit in seconds. + + \item[@{text default_type}] sets the type(s) generally used to instantiate type variables. - \<^descr>[@{text report}] if set quickcheck reports how many tests + \item[@{text report}] if set quickcheck reports how many tests fulfilled the preconditions. - \<^descr>[@{text use_subtype}] if set quickcheck automatically lifts + \item[@{text use_subtype}] if set quickcheck automatically lifts conjectures to registered subtypes if possible, and tests the lifted conjecture. - \<^descr>[@{text quiet}] if set quickcheck does not output anything + \item[@{text quiet}] if set quickcheck does not output anything while testing. - \<^descr>[@{text verbose}] if set quickcheck informs about the current + \item[@{text verbose}] if set quickcheck informs about the current size and cardinality while testing. - \<^descr>[@{text expect}] can be used to check if the user's + \item[@{text expect}] can be used to check if the user's expectation was met (@{text no_expectation}, @{text no_counterexample}, or @{text counterexample}). @@ -2035,7 +1955,7 @@ \begin{description} - \<^descr>[@{text exhaustive}] The parameters of the type classes @{class exhaustive} + \item[@{text exhaustive}] The parameters of the type classes @{class exhaustive} and @{class full_exhaustive} implement the testing. They take a testing function as a parameter, which takes a value of type @{typ "'a"} and optionally produces a counterexample, and a size parameter for the test values. @@ -2047,13 +1967,13 @@ testing function on all values up to the given size and stops as soon as a counterexample is found. - \<^descr>[@{text random}] The operation @{const Quickcheck_Random.random} + \item[@{text random}] The operation @{const Quickcheck_Random.random} of the type class @{class random} generates a pseudo-random value of the given size and a lazy term reconstruction of the value in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator is defined in theory @{theory Random}. - \<^descr>[@{text narrowing}] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"} + \item[@{text narrowing}] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"} using the type classes @{class narrowing} and @{class partial_term_of}. Variables in the current goal are initially represented as symbolic variables. If the execution of the goal tries to evaluate one of them, the test engine @@ -2111,8 +2031,6 @@ optional argument. If not provided, it checks the current theory. Options to the internal quickcheck invocations can be changed with common configuration declarations. - - \end{description} \ @@ -2142,8 +2060,6 @@ @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+) \} - \begin{description} - \<^descr> @{attribute (HOL) "coercion"}~@{text "f"} registers a new coercion function @{text "f :: \\<^sub>1 \ \\<^sub>2"} where @{text "\\<^sub>1"} and @{text "\\<^sub>2"} are type constructors without arguments. Coercions are @@ -2186,8 +2102,6 @@ \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference algorithm. - - \end{description} \ @@ -2200,8 +2114,6 @@ @{attribute_def (HOL) arith_split} & : & @{text attribute} \\ \end{matharray} - \begin{description} - \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types @{text nat}, @{text int}, @{text real}). Any current facts are inserted into the goal before running the procedure. @@ -2212,7 +2124,6 @@ \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be expanded before @{method (HOL) arith} is invoked. - \end{description} Note that a simpler (but faster) arithmetic prover is already invoked by the Simplifier. @@ -2230,8 +2141,6 @@ @@{method (HOL) iprover} (@{syntax rulemod} *) \} - \begin{description} - \<^descr> @{method (HOL) iprover} performs intuitionistic proof search, depending on specifically declared rules from the context, or given as explicit arguments. Chained facts are inserted into the goal @@ -2245,8 +2154,6 @@ single-step @{method (Pure) rule} method still observes these). An explicit weight annotation may be given as well; otherwise the number of rule premises will be taken into account here. - - \end{description} \ @@ -2266,8 +2173,6 @@ @{syntax thmrefs}? \} - \begin{description} - \<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure @{cite "loveland-78"}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for examples. @@ -2278,8 +2183,6 @@ Sledgehammer manual @{cite "isabelle-sledgehammer"} for details. The directory @{file "~~/src/HOL/Metis_Examples"} contains several small theories developed to a large extent using @{method (HOL) metis}. - - \end{description} \ @@ -2299,8 +2202,6 @@ @@{attribute (HOL) algebra} (() | 'add' | 'del') \} - \begin{description} - \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gr\"obner bases, see also @{cite "Chaieb-Wenzel:2007"} and @{cite \\S3.2\ "Chaieb-thesis"}. The method handles deals with two main @@ -2308,28 +2209,28 @@ \begin{enumerate} - \<^enum> Universal problems over multivariate polynomials in a - (semi)-ring/field/idom; the capabilities of the method are augmented - according to properties of these structures. For this problem class - the method is only complete for algebraically closed fields, since - the underlying method is based on Hilbert's Nullstellensatz, where - the equivalence only holds for algebraically closed fields. - - The problems can contain equations @{text "p = 0"} or inequations - @{text "q \ 0"} anywhere within a universal problem statement. - - \<^enum> All-exists problems of the following restricted (but useful) - form: - - @{text [display] "\x\<^sub>1 \ x\<^sub>n. - e\<^sub>1(x\<^sub>1, \, x\<^sub>n) = 0 \ \ \ e\<^sub>m(x\<^sub>1, \, x\<^sub>n) = 0 \ - (\y\<^sub>1 \ y\<^sub>k. - p\<^sub>1\<^sub>1(x\<^sub>1, \ ,x\<^sub>n) * y\<^sub>1 + \ + p\<^sub>1\<^sub>k(x\<^sub>1, \, x\<^sub>n) * y\<^sub>k = 0 \ - \ \ - p\<^sub>t\<^sub>1(x\<^sub>1, \, x\<^sub>n) * y\<^sub>1 + \ + p\<^sub>t\<^sub>k(x\<^sub>1, \, x\<^sub>n) * y\<^sub>k = 0)"} - - Here @{text "e\<^sub>1, \, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate - polynomials only in the variables mentioned as arguments. + \item Universal problems over multivariate polynomials in a + (semi)-ring/field/idom; the capabilities of the method are augmented + according to properties of these structures. For this problem class + the method is only complete for algebraically closed fields, since + the underlying method is based on Hilbert's Nullstellensatz, where + the equivalence only holds for algebraically closed fields. + + The problems can contain equations @{text "p = 0"} or inequations + @{text "q \ 0"} anywhere within a universal problem statement. + + \item All-exists problems of the following restricted (but useful) + form: + + @{text [display] "\x\<^sub>1 \ x\<^sub>n. + e\<^sub>1(x\<^sub>1, \, x\<^sub>n) = 0 \ \ \ e\<^sub>m(x\<^sub>1, \, x\<^sub>n) = 0 \ + (\y\<^sub>1 \ y\<^sub>k. + p\<^sub>1\<^sub>1(x\<^sub>1, \ ,x\<^sub>n) * y\<^sub>1 + \ + p\<^sub>1\<^sub>k(x\<^sub>1, \, x\<^sub>n) * y\<^sub>k = 0 \ + \ \ + p\<^sub>t\<^sub>1(x\<^sub>1, \, x\<^sub>n) * y\<^sub>1 + \ + p\<^sub>t\<^sub>k(x\<^sub>1, \, x\<^sub>n) * y\<^sub>k = 0)"} + + Here @{text "e\<^sub>1, \, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate + polynomials only in the variables mentioned as arguments. \end{enumerate} @@ -2340,8 +2241,6 @@ \<^descr> @{attribute algebra} (as attribute) manages the default collection of pre-simplification rules of the above proof method. - - \end{description} \ @@ -2380,14 +2279,10 @@ @@{method (HOL) coherent} @{syntax thmrefs}? \} - \begin{description} - \<^descr> @{method (HOL) coherent} solves problems of \emph{Coherent Logic} @{cite "Bezem-Coquand:2005"}, which covers applications in confluence theory, lattice theory and projective geometry. See @{file "~~/src/HOL/ex/Coherent.thy"} for some examples. - - \end{description} \ @@ -2417,8 +2312,6 @@ rule: 'rule' ':' @{syntax thmref} \} - \begin{description} - \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit to reason about inductive types. Rules are selected according to the declarations by the @{attribute cases} and @{attribute induct} @@ -2444,12 +2337,9 @@ for later use. The @{keyword "for"} argument of the @{method (HOL) ind_cases} method allows to specify a list of variables that should be generalized before applying the resulting rule. - - \end{description} \ - section \Adhoc tuples\ text \ @@ -2461,16 +2351,12 @@ @@{attribute (HOL) split_format} ('(' 'complete' ')')? \} - \begin{description} - \<^descr> @{attribute (HOL) split_format}\ @{text "(complete)"} causes arguments in function applications to be represented canonically according to their tuple type structure. Note that this operation tends to invent funny names for new local parameters introduced. - - \end{description} \ @@ -2601,8 +2487,6 @@ modes: mode @'as' const \} - \begin{description} - \<^descr> @{command (HOL) "export_code"} generates code for a given list of constants in the specified target language(s). If no serialization instruction is given, only abstract code is generated internally. @@ -2713,8 +2597,6 @@ which arguments are supposed to be input or output. If alternative introduction rules are declared, one must prove a corresponding elimination rule. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 16 14:53:26 2015 +0200 @@ -62,8 +62,6 @@ @{syntax_def modes}: '(' (@{syntax name} + ) ')' \} - \begin{description} - \<^descr> @{command "typ"}~@{text \} reads and prints a type expression according to the current context. @@ -101,7 +99,6 @@ \<^descr> @{command "print_state"} prints the current proof state (if present), including current facts and goals. - \end{description} All of the diagnostic commands above admit a list of @{text modes} to be specified, which is appended to the current print mode; see @@ -144,8 +141,6 @@ is displayed for types, terms, theorems, goals etc. See also \secref{sec:config}. - \begin{description} - \<^descr> @{attribute show_markup} controls direct inlining of markup into the printed representation of formal entities --- notably type and sort constraints. This enables Prover IDE users to retrieve @@ -238,8 +233,6 @@ question mark is affected, the remaining text is unchanged (including proper markup for schematic variables that might be relevant for user interfaces). - - \end{description} \ @@ -257,8 +250,6 @@ modes as optional argument. The underlying ML operations are as follows. - \begin{description} - \<^descr> @{ML "print_mode_value ()"} yields the list of currently active print mode names. This should be understood as symbolic representation of certain individual features for printing (with @@ -271,7 +262,6 @@ names: it retains the default print mode that certain user-interfaces might have installed for their proper functioning! - \end{description} \<^medskip> The pretty printer for inner syntax maintains alternative @@ -280,8 +270,6 @@ Mode names can be arbitrary, but the following ones have a specific meaning by convention: - \begin{itemize} - \<^item> @{verbatim \""\} (the empty string): default mode; implicitly active as last element in the list of modes. @@ -302,8 +290,6 @@ \<^item> @{verbatim latex}: additional mode that is active in {\LaTeX} document preparation of Isabelle theory sources; allows to provide alternative output notation. - - \end{itemize} \ @@ -377,8 +363,6 @@ general template format is a sequence over any of the following entities. - \begin{description} - \<^descr> @{text "d"} is a delimiter, namely a non-empty sequence of characters other than the following special characters: @@ -424,7 +408,6 @@ stands for the string of spaces (zero or more) right after the slash. These spaces are printed if the break is \emph{not} taken. - \end{description} The general idea of pretty printing with blocks and breaks is also described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}. @@ -532,8 +515,6 @@ @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and') \} - \begin{description} - \<^descr> @{command "type_notation"}~@{text "c (mx)"} associates mixfix syntax with an existing type constructor. The arity of the constructor is retrieved from the context. @@ -552,8 +533,6 @@ \<^descr> @{command "write"} is similar to @{command "notation"}, but works within an Isar proof body. - - \end{description} \ @@ -565,15 +544,12 @@ (\secref{sec:outer-lex}), but some details are different. There are two main categories of inner syntax tokens: - \begin{enumerate} - \<^enum> \emph{delimiters} --- the literal tokens occurring in productions of the given priority grammar (cf.\ \secref{sec:priority-grammar}); \<^enum> \emph{named tokens} --- various categories of identifiers etc. - \end{enumerate} Delimiters override named tokens and may thus render certain identifiers inaccessible. Sometimes the logical context admits @@ -659,7 +635,6 @@ \<^medskip> For clarity, grammars obey these conventions: - \begin{itemize} \<^item> All priorities must lie between 0 and 1000. @@ -675,7 +650,6 @@ \<^item> Repetition is indicated by dots @{text "(\)"} in an informal but obvious way. - \end{itemize} Using these conventions, the example grammar specification above takes the form: @@ -771,8 +745,6 @@ inner syntax. The meaning of the nonterminals defined by the above grammar is as follows: - \begin{description} - \<^descr> @{syntax_ref (inner) any} denotes any term. \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions, @@ -824,12 +796,9 @@ \<^descr> @{syntax_ref (inner) sort} denotes meta-level sorts. - \end{description} Here are some further explanations of certain syntax features. - \begin{itemize} - \<^item> In @{syntax (inner) idts}, note that @{text "x :: nat y"} is parsed as @{text "x :: (nat y)"}, treating @{text y} like a type constructor applied to @{text nat}. To avoid this interpretation, @@ -851,25 +820,25 @@ \begin{description} - \<^descr> A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an - anonymous inference parameter, which is filled-in according to the - most general type produced by the type-checking phase. + \item A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an + anonymous inference parameter, which is filled-in according to the + most general type produced by the type-checking phase. - \<^descr> A bound ``@{text "_"}'' refers to a vacuous abstraction, where - the body does not refer to the binding introduced here. As in the - term @{term "\x _. x"}, which is @{text "\"}-equivalent to @{text - "\x y. x"}. + \item A bound ``@{text "_"}'' refers to a vacuous abstraction, where + the body does not refer to the binding introduced here. As in the + term @{term "\x _. x"}, which is @{text "\"}-equivalent to @{text + "\x y. x"}. - \<^descr> A free ``@{text "_"}'' refers to an implicit outer binding. - Higher definitional packages usually allow forms like @{text "f x _ - = x"}. + \item A free ``@{text "_"}'' refers to an implicit outer binding. + Higher definitional packages usually allow forms like @{text "f x _ + = x"}. - \<^descr> A schematic ``@{text "_"}'' (within a term pattern, see - \secref{sec:term-decls}) refers to an anonymous variable that is - implicitly abstracted over its context of locally bound variables. - For example, this allows pattern matching of @{text "{x. f x = g - x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by - using both bound and schematic dummies. + \item A schematic ``@{text "_"}'' (within a term pattern, see + \secref{sec:term-decls}) refers to an anonymous variable that is + implicitly abstracted over its context of locally bound variables. + For example, this allows pattern matching of @{text "{x. f x = g + x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by + using both bound and schematic dummies. \end{description} @@ -887,8 +856,6 @@ \<^descr> @{verbatim XCONST} is similar to @{verbatim CONST}, but retains the constant name as given. This is only relevant to translation rules (\secref{sec:syn-trans}), notably on the LHS. - - \end{itemize} \ @@ -899,54 +866,50 @@ @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} - \begin{description} - \<^descr> @{command "print_syntax"} prints the inner syntax of the current context. The output can be quite large; the most important sections are explained below. \begin{description} - \<^descr> @{text "lexicon"} lists the delimiters of the inner token - language; see \secref{sec:inner-lex}. + \item @{text "lexicon"} lists the delimiters of the inner token + language; see \secref{sec:inner-lex}. - \<^descr> @{text "prods"} lists the productions of the underlying - priority grammar; see \secref{sec:priority-grammar}. + \item @{text "prods"} lists the productions of the underlying + priority grammar; see \secref{sec:priority-grammar}. - The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text - "A[p]"}; delimiters are quoted. Many productions have an extra - @{text "\ => name"}. These names later become the heads of parse - trees; they also guide the pretty printer. + The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text + "A[p]"}; delimiters are quoted. Many productions have an extra + @{text "\ => name"}. These names later become the heads of parse + trees; they also guide the pretty printer. - Productions without such parse tree names are called \emph{copy - productions}. Their right-hand side must have exactly one - nonterminal symbol (or named token). The parser does not create a - new parse tree node for copy productions, but simply returns the - parse tree of the right-hand symbol. + Productions without such parse tree names are called \emph{copy + productions}. Their right-hand side must have exactly one + nonterminal symbol (or named token). The parser does not create a + new parse tree node for copy productions, but simply returns the + parse tree of the right-hand symbol. - If the right-hand side of a copy production consists of a single - nonterminal without any delimiters, then it is called a \emph{chain - production}. Chain productions act as abbreviations: conceptually, - they are removed from the grammar by adding new productions. - Priority information attached to chain productions is ignored; only - the dummy value @{text "-1"} is displayed. + If the right-hand side of a copy production consists of a single + nonterminal without any delimiters, then it is called a \emph{chain + production}. Chain productions act as abbreviations: conceptually, + they are removed from the grammar by adding new productions. + Priority information attached to chain productions is ignored; only + the dummy value @{text "-1"} is displayed. - \<^descr> @{text "print modes"} lists the alternative print modes - provided by this grammar; see \secref{sec:print-modes}. + \item @{text "print modes"} lists the alternative print modes + provided by this grammar; see \secref{sec:print-modes}. - \<^descr> @{text "parse_rules"} and @{text "print_rules"} relate to - syntax translations (macros); see \secref{sec:syn-trans}. + \item @{text "parse_rules"} and @{text "print_rules"} relate to + syntax translations (macros); see \secref{sec:syn-trans}. - \<^descr> @{text "parse_ast_translation"} and @{text - "print_ast_translation"} list sets of constants that invoke - translation functions for abstract syntax trees, which are only - required in very special situations; see \secref{sec:tr-funs}. + \item @{text "parse_ast_translation"} and @{text + "print_ast_translation"} list sets of constants that invoke + translation functions for abstract syntax trees, which are only + required in very special situations; see \secref{sec:tr-funs}. - \<^descr> @{text "parse_translation"} and @{text "print_translation"} - list the sets of constants that invoke regular translation - functions; see \secref{sec:tr-funs}. - - \end{description} + \item @{text "parse_translation"} and @{text "print_translation"} + list the sets of constants that invoke regular translation + functions; see \secref{sec:tr-funs}. \end{description} \ @@ -974,16 +937,12 @@ situation and the given configuration options. Parsing ultimately fails, if multiple results remain after the filtering phase. - \begin{description} - \<^descr> @{attribute syntax_ambiguity_warning} controls output of explicit warning messages about syntax ambiguity. \<^descr> @{attribute syntax_ambiguity_limit} determines the number of resulting parse trees that are shown as part of the printed message in case of an ambiguity. - - \end{description} \ @@ -1133,8 +1092,6 @@ bound variables is excluded as well. Authentic syntax names work implicitly in the following situations: - \begin{itemize} - \<^item> Input of term constants (or fixed variables) that are introduced by concrete syntax via @{command notation}: the correspondence of a particular grammar production to some known term @@ -1148,7 +1105,6 @@ this information is already available from the internal term to be printed. - \end{itemize} In other words, syntax transformations that operate on input terms written as prefix applications are difficult to make robust. @@ -1195,8 +1151,6 @@ transpat: ('(' @{syntax nameref} ')')? @{syntax string} \} - \begin{description} - \<^descr> @{command "nonterminal"}~@{text c} declares a type constructor @{text c} (without arguments) to act as purely syntactic type: a nonterminal symbol of the inner syntax. @@ -1215,15 +1169,15 @@ follows: \begin{itemize} - \<^item> @{text "prop"} if @{text "\\<^sub>i = prop"} + \item @{text "prop"} if @{text "\\<^sub>i = prop"} - \<^item> @{text "logic"} if @{text "\\<^sub>i = (\)\"} for logical type - constructor @{text "\ \ prop"} + \item @{text "logic"} if @{text "\\<^sub>i = (\)\"} for logical type + constructor @{text "\ \ prop"} - \<^item> @{text any} if @{text "\\<^sub>i = \"} for type variables + \item @{text any} if @{text "\\<^sub>i = \"} for type variables - \<^item> @{text "\"} if @{text "\\<^sub>i = \"} for nonterminal @{text "\"} - (syntactic type constructor) + \item @{text "\"} if @{text "\\<^sub>i = \"} for nonterminal @{text "\"} + (syntactic type constructor) \end{itemize} @@ -1291,14 +1245,14 @@ \begin{itemize} - \<^item> Rules must be left linear: @{text "lhs"} must not contain - repeated variables.\footnote{The deeper reason for this is that AST - equality is not well-defined: different occurrences of the ``same'' - AST could be decorated differently by accidental type-constraints or - source position information, for example.} + \item Rules must be left linear: @{text "lhs"} must not contain + repeated variables.\footnote{The deeper reason for this is that AST + equality is not well-defined: different occurrences of the ``same'' + AST could be decorated differently by accidental type-constraints or + source position information, for example.} - \<^item> Every variable in @{text "rhs"} must also occur in @{text - "lhs"}. + \item Every variable in @{text "rhs"} must also occur in @{text + "lhs"}. \end{itemize} @@ -1311,7 +1265,6 @@ process, when translation rules are applied to concrete input or output. - \end{description} Raw syntax and translations provides a slightly more low-level access to the grammar and the form of resulting parse trees. It is @@ -1320,8 +1273,6 @@ Some important situations where @{command syntax} and @{command translations} are really need are as follows: - \begin{itemize} - \<^item> Iterated replacement via recursive @{command translations}. For example, consider list enumeration @{term "[a, b, c, d]"} as defined in theory @{theory List} in Isabelle/HOL. @@ -1331,9 +1282,8 @@ syntax translations. For example, consider list filter comprehension @{term "[x \ xs . P]"} as defined in theory @{theory List} in Isabelle/HOL. +\ - \end{itemize} -\ subsubsection \Applying translation rules\ @@ -1356,8 +1306,6 @@ More precisely, the matching of the object @{text "u"} against the pattern @{text "lhs"} is performed as follows: - \begin{itemize} - \<^item> Objects of the form @{ML Ast.Variable}~@{text "x"} or @{ML Ast.Constant}~@{text "x"} are matched by pattern @{ML Ast.Constant}~@{text "x"}. Thus all atomic ASTs in the object are @@ -1374,7 +1322,6 @@ \<^item> In every other case, matching fails. - \end{itemize} A successful match yields a substitution that is applied to @{text "rhs"}, generating the instance that replaces @{text "u"}. @@ -1439,8 +1386,6 @@ @@{ML_antiquotation syntax_const}) name \} - \begin{description} - \<^descr> @{command parse_translation} etc. declare syntax translation functions to the theory. Any of these commands have a single @{syntax text} argument that refers to an ML expression of @@ -1486,8 +1431,6 @@ that the usual naming convention makes syntax constants start with underscore, to reduce the chance of accidental clashes with other names occurring in parse trees (unqualified constants etc.). - - \end{description} \ @@ -1515,8 +1458,6 @@ functions called during the parsing process differ from those for printing in their overall behaviour: - \begin{description} - \<^descr>[Parse translations] are applied bottom-up. The arguments are already in translated form. The translations must not fail; exceptions trigger an error message. There may be at most one @@ -1531,7 +1472,6 @@ some syntactic name are tried in the order of declaration in the theory. - \end{description} Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and @{ML Const} for terms --- can invoke translation functions. This diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 16 14:53:26 2015 +0200 @@ -47,15 +47,11 @@ @@{command help} (@{syntax name} * ) \} - \begin{description} - \<^descr> @{command "print_commands"} prints all outer syntax keywords and commands. \<^descr> @{command "help"}~@{text "pats"} retrieves outer syntax commands according to the specified name patterns. - - \end{description} \ @@ -73,8 +69,6 @@ text \The outer lexical syntax consists of three main categories of syntax tokens: - \begin{enumerate} - \<^enum> \emph{major keywords} --- the command names that are available in the present logic session; @@ -83,7 +77,6 @@ \<^enum> \emph{named tokens} --- various categories of identifiers etc. - \end{enumerate} Major keywords and minor keywords are guaranteed to be disjoint. This helps user-interfaces to determine the overall structure of a @@ -412,7 +405,6 @@ result. There are three forms of theorem references: - \begin{enumerate} \<^enum> named facts @{text "a"}, @@ -422,7 +414,6 @@ @{verbatim "`"}@{text "\"}@{verbatim "`"} or @{syntax_ref cartouche} @{text "\\\"} (see also method @{method_ref fact}). - \end{enumerate} Any kind of theorem specification may include lists of attributes both on the left and right hand sides; attributes are applied to any @@ -503,8 +494,6 @@ Note that there are some further ones available, such as for the set of rules declared for simplifications. - \begin{description} - \<^descr> @{command "print_theory"} prints the main logical content of the background theory; the ``@{text "!"}'' option indicates extra verbosity. @@ -575,8 +564,6 @@ If @{text n} is @{text 0}, the end of the range of theories defaults to the current theory. If no range is specified, only the unused theorems in the current theory are displayed. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Fri Oct 16 14:53:26 2015 +0200 @@ -11,8 +11,6 @@ facts, and open goals. Isar/VM transitions are typed according to the following three different modes of operation: - \begin{description} - \<^descr> @{text "proof(prove)"} means that a new goal has just been stated that is now to be \emph{proven}; the next command may refine it by some proof method, and enter a sub-proof to establish the @@ -27,7 +25,6 @@ contents of the special @{fact_ref this} register) have been just picked up in order to be used when refining the goal claimed next. - \end{description} The proof mode indicator may be understood as an instruction to the writer, telling what kind of operation may be performed next. The @@ -58,13 +55,9 @@ @@{command end} \} - \begin{description} - \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without any goal statement. This allows to experiment with Isar, without producing any persistent result. The notepad is closed by @{command "end"}. - - \end{description} \ @@ -91,8 +84,6 @@ parentheses as well. These typically achieve a stronger forward style of reasoning. - \begin{description} - \<^descr> @{command "next"} switches to a fresh block within a sub-proof, resetting the local context to the initial one. @@ -105,8 +96,6 @@ of @{command "assume"} and @{command "presume"} in this mode of forward reasoning --- in contrast to plain backward reasoning with the result exported at @{command "show"} time. - - \end{description} \ @@ -190,8 +179,6 @@ @{syntax name} ('==' | '\') @{syntax term} @{syntax term_pat}? \} - \begin{description} - \<^descr> @{command "fix"}~@{text x} introduces a local variable @{text x} that is \emph{arbitrary, but fixed.} @@ -215,8 +202,6 @@ The default name for the definitional equation is @{text x_def}. Several simultaneous definitions may be given at the same time. - - \end{description} \ @@ -262,8 +247,6 @@ The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or @{syntax prop_pat} (see \secref{sec:term-decls}). - \begin{description} - \<^descr> @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \ \ p\<^sub>n = t\<^sub>n"} binds any text variables in patterns @{text "p\<^sub>1, \, p\<^sub>n"} by simultaneous higher-order matching against terms @{text "t\<^sub>1, \, t\<^sub>n"}. @@ -273,7 +256,6 @@ note that @{keyword "is"} is not a separate command, but part of others (such as @{command "assume"}, @{command "have"} etc.). - \end{description} Some \emph{implicit} term abbreviations\index{term abbreviations} for goals and facts are available as well. For any open goal, @@ -318,8 +300,6 @@ (@{syntax thmrefs} + @'and') \} - \begin{description} - \<^descr> @{command "note"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} recalls existing facts @{text "b\<^sub>1, \, b\<^sub>n"}, binding the result as @{text a}. Note that attributes may be involved as well, both on the left and right hand @@ -351,7 +331,6 @@ similar to @{command "using"}, but unfolds definitional equations @{text "b\<^sub>1, \ b\<^sub>n"} throughout the goal state and facts. - \end{description} Forward chaining with an empty list of theorems is the same as not chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no @@ -443,8 +422,6 @@ (@{syntax thmdecl}? (@{syntax prop}+) + @'and') \} - \begin{description} - \<^descr> @{command "lemma"}~@{text "a: \"} enters proof mode with @{text \} as main goal, eventually resulting in some fact @{text "\ \"} to be put back into the target context. An additional @{syntax @@ -500,7 +477,6 @@ current theory or proof context in long statement form, according to the syntax for @{command "lemma"} given above. - \end{description} Any goal statement causes some term abbreviations (such as @{variable_ref "?thesis"}) to be bound automatically, see also @@ -574,8 +550,6 @@ @@{attribute trans} (() | 'add' | 'del') \} - \begin{description} - \<^descr> @{command "also"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintains the auxiliary @{fact calculation} register as follows. The first occurrence of @{command "also"} in some calculational thread initializes @{fact @@ -620,8 +594,6 @@ explicit single-step elimination proof, such as ``@{command "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text "y = x"}~@{command ".."}''. - - \end{description} \ @@ -704,8 +676,6 @@ Structured proof composition in Isar admits proof methods to be invoked in two places only. - \begin{enumerate} - \<^enum> An \emph{initial} refinement step @{command_ref "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number of sub-goals that are to be solved later. Facts are passed to @@ -716,7 +686,6 @@ "m\<^sub>2"} is intended to solve remaining goals. No facts are passed to @{text "m\<^sub>2"}. - \end{enumerate} The only other (proper) way to affect pending goals in a proof body is by @{command_ref "show"}, which involves an explicit statement of @@ -749,8 +718,6 @@ (@@{command "."} | @@{command ".."} | @@{command sorry}) \} - \begin{description} - \<^descr> @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof method @{text "m\<^sub>1"}; facts for forward chaining are passed if so indicated by @{text "proof(chain)"} mode. @@ -808,8 +775,6 @@ In Isabelle/HOL, @{method standard} also takes classical rules into account (cf.\ \secref{sec:classical}). - - \end{description} \ @@ -860,8 +825,6 @@ @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes} \} - \begin{description} - \<^descr> @{command "print_rules"} prints rules declared via attributes @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of Isabelle/Pure. @@ -970,8 +933,6 @@ An optional context of local variables @{text "\ x\<^sub>1 \ x\<^sub>m"} may be specified as for @{attribute "of"} above. - - \end{description} \ @@ -986,8 +947,6 @@ @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}? \} - \begin{description} - \<^descr> @{command "method_setup"}~@{text "name = text description"} defines a proof method in the current context. The given @{text "text"} has to be an ML expression of type @@ -999,8 +958,6 @@ addressing. Here are some example method definitions: - - \end{description} \ (*<*)experiment begin(*>*) @@ -1094,8 +1051,6 @@ @@{attribute consumes} @{syntax int}? \} - \begin{description} - \<^descr> @{command "case"}~@{text "a: (c x\<^sub>1 \ x\<^sub>m)"} invokes a named local context @{text "c: x\<^sub>1, \, x\<^sub>m, \\<^sub>1, \, \\<^sub>m"}, as provided by an appropriate proof method (such as @{method_ref cases} and @{method_ref @@ -1158,8 +1113,6 @@ rarely needed; this is already taken care of automatically by the higher-level @{attribute cases}, @{attribute induct}, and @{attribute coinduct} declarations. - - \end{description} \ @@ -1214,8 +1167,6 @@ taking: 'taking' ':' @{syntax insts} \} - \begin{description} - \<^descr> @{method cases}~@{text "insts R"} applies method @{method rule} with an appropriate case distinction theorem, instantiated to the subjects @{text insts}. Symbolic case names are bound according @@ -1327,7 +1278,6 @@ specification may be required in order to specify the bisimulation to be used in the coinduction step. - \end{description} Above methods produce named local contexts, as determined by the instantiated rule as given in the text. Beyond that, the @{method @@ -1404,8 +1354,6 @@ spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del' \} - \begin{description} - \<^descr> @{command "print_induct_rules"} prints cases and induct rules for predicates (or sets) and types of the current context. @@ -1428,8 +1376,6 @@ declaration is taken care of automatically: @{attribute consumes}~@{text 0} is specified for ``type'' rules and @{attribute consumes}~@{text 1} for ``predicate'' / ``set'' rules. - - \end{description} \ @@ -1470,8 +1416,6 @@ @@{command guess} (@{syntax "fixes"} + @'and') \} - \begin{description} - \<^descr> @{command consider}~@{text "(a) \<^vec>x \ \<^vec>A \<^vec>x | (b) \<^vec>y \ \<^vec>B \<^vec>y | \ "} states a rule for case splitting into separate subgoals, such that each case involves new @@ -1543,7 +1487,6 @@ The variable names and type constraints given as arguments for @{command "guess"} specify a prefix of accessible parameters. - \end{description} In the proof of @{command consider} and @{command obtain} the local premises are always bound to the fact name @{fact_ref that}, according to diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Proof_Script.thy --- a/src/Doc/Isar_Ref/Proof_Script.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Proof_Script.thy Fri Oct 16 14:53:26 2015 +0200 @@ -41,8 +41,6 @@ @@{command prefer} @{syntax nat} \} - \begin{description} - \<^descr> @{command "supply"} supports fact definitions during goal refinement: it is similar to @{command "note"}, but it operates in backwards mode and does not have any impact on chained facts. @@ -83,8 +81,6 @@ results, and this command explores the possibilities step-by-step. It is mainly useful for experimentation and interactive exploration, and should be avoided in finished proofs. - - \end{description} \ @@ -103,8 +99,6 @@ params: @'for' '\'? (('_' | @{syntax name})+) \} - \begin{description} - \<^descr> @{command "subgoal"} allows to impose some structure on backward refinements, to avoid proof scripts degenerating into long of @{command apply} sequences. @@ -133,7 +127,6 @@ of a proven subgoal. Thus it may be re-used in further reasoning, similar to the result of @{command show} in structured Isar proofs. - \end{description} Here are some abstract examples: \ @@ -245,8 +238,6 @@ (@@{method tactic} | @@{method raw_tactic}) @{syntax text} \} -\begin{description} - \<^descr> @{method rule_tac} etc. do resolution of rules with explicit instantiation. This works the same way as the ML tactics @{ML Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}). @@ -294,8 +285,6 @@ the usual split into several subgoals. While feature this is useful for debugging of complex method definitions, it should not never appear in production theories. - - \end{description} \ end \ No newline at end of file diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Fri Oct 16 14:53:26 2015 +0200 @@ -72,8 +72,6 @@ thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')' \} - \begin{description} - \<^descr> @{command "theory"}~@{text "A \ B\<^sub>1 \ B\<^sub>n \"} starts a new theory @{text A} based on the merge of existing theories @{text "B\<^sub>1 \ B\<^sub>n"}. Due to the possibility to import more @@ -115,8 +113,6 @@ base session as a starting point. Alternatively, it is possibly to restrict the full theory graph by giving bounds, analogously to @{command_ref class_deps}. - - \end{description} \ @@ -153,8 +149,6 @@ @{syntax_def target}: '(' @'in' @{syntax nameref} ')' \} - \begin{description} - \<^descr> @{command "context"}~@{text "c \"} opens a named context, by recommencing an existing locale or class @{text c}. Note that locale and class definitions allow to include the @@ -193,7 +187,6 @@ ``@{text "(\ -)"}'' will always produce a global result independently of the current target context. - \end{description} Any specification element that operates on @{text local_theory} according to this manual implicitly allows the above target syntax @{text @@ -256,8 +249,6 @@ @{syntax_def "includes"}: @'includes' (@{syntax nameref}+) \} - \begin{description} - \<^descr> @{command bundle}~@{text "b = decls"} defines a bundle of declarations in the current context. The RHS is similar to the one of the @{command declare} command. Bundles defined in local theory @@ -284,10 +275,10 @@ context is constructed, notably for @{command context} and long statements of @{command theorem} etc. - \end{description} Here is an artificial example of bundling various configuration - options:\ + options: +\ (*<*)experiment begin(*>*) bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]] @@ -324,8 +315,6 @@ @@{command print_abbrevs} ('!'?) \} - \begin{description} - \<^descr> @{command "definition"}~@{text "c \ eq"} produces an internal definition @{text "c \ t"} according to the specification given as @{text eq}, which is then turned into a proven fact. The @@ -362,8 +351,6 @@ \<^descr> @{command "print_abbrevs"} prints all constant abbreviations of the current context; the ``@{text "!"}'' option indicates extra verbosity. - - \end{description} \ @@ -380,8 +367,6 @@ specs: (@{syntax thmdecl}? @{syntax props} + @'and') \} - \begin{description} - \<^descr> @{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m \ \\<^sub>1 \ \\<^sub>n"} introduces several constants simultaneously and states axiomatic properties for these. The constants are marked as being specified once and @@ -400,8 +385,6 @@ within Isabelle/Pure, but in an application environment like Isabelle/HOL the user normally stays within definitional mechanisms provided by the logic and its libraries. - - \end{description} \ @@ -430,8 +413,6 @@ @@{command declare} (@{syntax thmrefs} + @'and') \} - \begin{description} - \<^descr> @{command "declaration"}~@{text d} adds the declaration function @{text d} of ML type @{ML_type declaration}, to the current local theory under construction. In later application contexts, the @@ -451,8 +432,6 @@ unlike @{command "lemmas"} (cf.\ \secref{sec:theorems}), so @{command "declare"} only has the effect of applying attributes as included in the theorem specification. - - \end{description} \ @@ -563,8 +542,6 @@ @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and') \} - \begin{description} - \<^descr> @{command "locale"}~@{text "loc = import + body"} defines a new locale @{text loc} as a context consisting of a certain view of existing locales (@{text import}) plus some additional elements @@ -590,32 +567,32 @@ \begin{description} - \<^descr> @{element "fixes"}~@{text "x :: \ (mx)"} declares a local - parameter of type @{text \} and mixfix annotation @{text mx} (both - are optional). The special syntax declaration ``@{text - "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may - be referenced implicitly in this context. + \item @{element "fixes"}~@{text "x :: \ (mx)"} declares a local + parameter of type @{text \} and mixfix annotation @{text mx} (both + are optional). The special syntax declaration ``@{text + "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may + be referenced implicitly in this context. - \<^descr> @{element "constrains"}~@{text "x :: \"} introduces a type - constraint @{text \} on the local parameter @{text x}. This - element is deprecated. The type constraint should be introduced in - the @{keyword "for"} clause or the relevant @{element "fixes"} element. + \item @{element "constrains"}~@{text "x :: \"} introduces a type + constraint @{text \} on the local parameter @{text x}. This + element is deprecated. The type constraint should be introduced in + the @{keyword "for"} clause or the relevant @{element "fixes"} element. - \<^descr> @{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"} - introduces local premises, similar to @{command "assume"} within a - proof (cf.\ \secref{sec:proof-context}). + \item @{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"} + introduces local premises, similar to @{command "assume"} within a + proof (cf.\ \secref{sec:proof-context}). - \<^descr> @{element "defines"}~@{text "a: x \ t"} defines a previously - declared parameter. This is similar to @{command "def"} within a - proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} - takes an equational proposition instead of variable-term pair. The - left-hand side of the equation may have additional arguments, e.g.\ - ``@{element "defines"}~@{text "f x\<^sub>1 \ x\<^sub>n \ t"}''. + \item @{element "defines"}~@{text "a: x \ t"} defines a previously + declared parameter. This is similar to @{command "def"} within a + proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} + takes an equational proposition instead of variable-term pair. The + left-hand side of the equation may have additional arguments, e.g.\ + ``@{element "defines"}~@{text "f x\<^sub>1 \ x\<^sub>n \ t"}''. - \<^descr> @{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} - reconsiders facts within a local context. Most notably, this may - include arbitrary declarations in any attribute specifications - included here, e.g.\ a local @{attribute simp} rule. + \item @{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} + reconsiders facts within a local context. Most notably, this may + include arbitrary declarations in any attribute specifications + included here, e.g.\ a local @{attribute simp} rule. \end{description} @@ -676,8 +653,6 @@ specifications entailed by the context, both from target statements, and from interpretations (see below). New goals that are entailed by the current context are discharged automatically. - - \end{description} \ @@ -716,8 +691,6 @@ equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') \} - \begin{description} - \<^descr> @{command "interpretation"}~@{text "expr \ eqns"} interprets @{text expr} in a global or local theory. The command generates proof obligations for the instantiated specifications. @@ -814,7 +787,6 @@ "interpretation"} or @{command "interpret"} and one or several @{command "sublocale"} declarations. - \end{description} \begin{warn} If a global theory inherits declarations (body elements) for a @@ -851,13 +823,10 @@ available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"} and provides - \begin{enumerate} - \<^enum> a unified view on arbitrary suitable local theories as interpretation target; \<^enum> rewrite morphisms by means of \emph{rewrite definitions}. - \end{enumerate} \begin{matharray}{rcl} @{command_def "permanent_interpretation"} & : & @{text "local_theory \ proof(prove)"} @@ -872,8 +841,6 @@ equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') \} - \begin{description} - \<^descr> @{command "permanent_interpretation"}~@{text "expr \ defs \ eqns"} interprets @{text expr} in the current local theory. The command generates proof obligations for the instantiated specifications. @@ -900,12 +867,12 @@ \begin{itemize} - \<^item> produces a corresponding definition in - the local theory's underlying target \emph{and} - - \<^item> augments the rewrite morphism with the equation - stemming from the symmetric of the corresponding definition. - + \item produces a corresponding definition in + the local theory's underlying target \emph{and} + + \item augments the rewrite morphism with the equation + stemming from the symmetric of the corresponding definition. + \end{itemize} This is technically different to to a naive combination @@ -913,18 +880,16 @@ \begin{itemize} - \<^item> Definitions are parsed in the syntactic interpretation - context, just like equations. + \item Definitions are parsed in the syntactic interpretation + context, just like equations. - \<^item> The proof needs not consider the equations stemming from - definitions -- they are proved implicitly by construction. + \item The proof needs not consider the equations stemming from + definitions -- they are proved implicitly by construction. \end{itemize} Rewrite definitions yield a pattern for introducing new explicit operations for existing terms after interpretation. - - \end{description} \ @@ -970,8 +935,6 @@ class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')' \} - \begin{description} - \<^descr> @{command "class"}~@{text "c = superclasses + body"} defines a new class @{text c}, inheriting from @{text superclasses}. This introduces a locale @{text c} with import of all locales @{text @@ -1044,8 +1007,6 @@ default proof step (e.g.\ of @{command "proof"}). In particular, instantiation of trivial (syntactic) classes may be performed by a single ``@{command ".."}'' proof step. - - \end{description} \ @@ -1058,8 +1019,6 @@ If this locale is also a class @{text c}, apart from the common locale target behaviour the following happens. - \begin{itemize} - \<^item> Local constant declarations @{text "g[\]"} referring to the local type parameter @{text \} and local parameters @{text "f[\]"} are accompanied by theory-level constants @{text "g[?\ :: c]"} @@ -1071,8 +1030,6 @@ global operations @{text "g[?\ :: c]"} uniformly. Type inference resolves ambiguities. In rare cases, manual type annotations are needed. - - \end{itemize} \ @@ -1141,8 +1098,6 @@ spec: @{syntax name} ( '==' | '\' ) @{syntax term} ( '(' @'unchecked' ')' )? \} - \begin{description} - \<^descr> @{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"} opens a theory target (cf.\ \secref{sec:target}) which allows to specify constants with overloaded definitions. These are identified @@ -1158,8 +1113,6 @@ exotic overloading (see \secref{sec:consts} for a precise description). It is at the discretion of the user to avoid malformed theory specifications! - - \end{description} \ @@ -1192,8 +1145,6 @@ @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? \} - \begin{description} - \<^descr> @{command "SML_file"}~@{text "name"} reads and evaluates the given Standard ML file. Top-level SML bindings are stored within the theory context; the initial environment is restricted to the @@ -1245,8 +1196,6 @@ In principle, attributes can operate both on a given theorem and the implicit context, although in practice only one is modified and the other serves as parameter. Here are examples for these two cases: - - \end{description} \ (*<*)experiment begin(*>*) @@ -1266,8 +1215,6 @@ (*<*)end(*>*) text \ - \begin{description} - \<^descr> @{attribute ML_print_depth} controls the printing depth of the ML toplevel pretty printer; the precise effect depends on the ML compiler and run-time system. Typically the limit should be less than 10. Bigger values @@ -1288,8 +1235,6 @@ Runtime.exn_trace} into ML code for debugging @{cite "isabelle-implementation"}, closer to the point where it actually happens. - - \end{description} \ @@ -1306,8 +1251,6 @@ @@{command default_sort} @{syntax sort} \} - \begin{description} - \<^descr> @{command "default_sort"}~@{text s} makes sort @{text s} the new default sort for any type variable that is given explicitly in the text, but lacks a sort constraint (wrt.\ the current context). @@ -1320,8 +1263,6 @@ When merging theories, the default sorts of the parents are logically intersected, i.e.\ the representations as lists of classes are joined. - - \end{description} \ @@ -1339,8 +1280,6 @@ @@{command typedecl} @{syntax typespec} @{syntax mixfix}? \} - \begin{description} - \<^descr> @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces a \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the existing type @{text "\"}. Unlike the semantic type definitions in Isabelle/HOL, type synonyms @@ -1352,7 +1291,6 @@ @{text s}, then the constructor is declared to operate on that, via the axiomatic type-class instance @{text "t :: (s, \, s)s"}. - \end{description} \begin{warn} If you introduce a new type axiomatically, i.e.\ via @{command_ref @@ -1389,8 +1327,6 @@ The built-in well-formedness conditions for definitional specifications are: - \begin{itemize} - \<^item> Arguments (on the left-hand side) must be distinct variables. \<^item> All variables on the right-hand side must also appear on the @@ -1404,7 +1340,6 @@ provide definitional principles that can be used to express recursion safely. - \end{itemize} The right-hand side of overloaded definitions may mention overloaded constants recursively at type instances corresponding to the immediate @@ -1422,8 +1357,6 @@ opt: '(' @'unchecked'? @'overloaded'? ')' \} - \begin{description} - \<^descr> @{command "consts"}~@{text "c :: \"} declares constant @{text c} to have any instance of type scheme @{text \}. The optional mixfix annotations may attach concrete syntax to the constants @@ -1441,8 +1374,6 @@ potentially overloaded. Unless this option is given, a warning message would be issued for any definitional equation with a more special type than that of the corresponding constant declaration. - - \end{description} \ @@ -1461,8 +1392,6 @@ @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and') \} - \begin{description} - \<^descr> @{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}~@{keyword_def "for"}~@{text "x\<^sub>1 \ x\<^sub>m"} evaluates given facts (with attributes) in the current context, which may be augmented by local variables. @@ -1474,8 +1403,6 @@ an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the content incrementally, in canonical declaration order of the text structure. - - \end{description} \ @@ -1505,8 +1432,6 @@ @@{command oracle} @{syntax name} '=' @{syntax text} \} - \begin{description} - \<^descr> @{command "oracle"}~@{text "name = text"} turns the given ML expression @{text "text"} of type @{ML_text "'a -> cterm"} into an ML function of type @{ML_text "'a -> thm"}, which is bound to the @@ -1514,7 +1439,6 @@ specification of axioms! Invoking the oracle only works within the scope of the resulting theory. - \end{description} See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of defining a new primitive rule as oracle, and turning it into a proof @@ -1543,8 +1467,6 @@ name spaces by hand, yet the following commands provide some way to do so. - \begin{description} - \<^descr> @{command "hide_class"}~@{text names} fully removes class declarations from a given name space; with the @{text "(open)"} option, only the unqualified base name is hidden. @@ -1557,8 +1479,6 @@ \<^descr> @{command "hide_type"}, @{command "hide_const"}, and @{command "hide_fact"} are similar to @{command "hide_class"}, but hide types, constants, and facts, respectively. - - \end{description} \ end diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Isar_Ref/Synopsis.thy --- a/src/Doc/Isar_Ref/Synopsis.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Isar_Ref/Synopsis.thy Fri Oct 16 14:53:26 2015 +0200 @@ -129,8 +129,6 @@ subsubsection \Naming conventions\ text \ - \begin{itemize} - \<^item> Lower-case identifiers are usually preferred. \<^item> Facts can be named after the main term within the proposition. @@ -144,8 +142,6 @@ \<^item> Symbolic identifiers are supported (e.g. @{text "*"}, @{text "**"}, @{text "***"}). - - \end{itemize} \ @@ -224,8 +220,6 @@ subsection \Special names in Isar proofs\ text \ - \begin{itemize} - \<^item> term @{text "?thesis"} --- the main conclusion of the innermost pending claim @@ -233,8 +227,6 @@ stated result (for infix application this is the right-hand side) \<^item> fact @{text "this"} --- the last result produced in the text - - \end{itemize} \ notepad @@ -313,15 +305,11 @@ subsubsection \Notes\ text \ - \begin{itemize} - \<^item> The notion of @{text trans} rule is very general due to the flexibility of Isabelle/Pure rule composition. \<^item> User applications may declare their own rules, with some care about the operational details of higher-order unification. - - \end{itemize} \ @@ -391,7 +379,6 @@ In practice, much more proof infrastructure is required. The proof method @{method induct} provides: - \begin{itemize} \<^item> implicit rule selection and robust instantiation @@ -399,8 +386,6 @@ \<^item> support for rule-structured induction statements, with local parameters, premises, etc. - - \end{itemize} \ notepad @@ -421,7 +406,6 @@ text \ The subsequent example combines the following proof patterns: - \begin{itemize} \<^item> outermost induction (over the datatype structure of natural numbers), to decompose the proof problem in top-down manner @@ -430,8 +414,6 @@ to compose the result in each case \<^item> solving local claims within the calculation by simplification - - \end{itemize} \ lemma @@ -682,16 +664,14 @@ text \ The Pure framework provides means for: - \begin{itemize} - \<^item> backward-chaining of rules by @{inference resolution} \<^item> closing of branches by @{inference assumption} - \end{itemize} Both principles involve higher-order unification of @{text \}-terms - modulo @{text "\\\"}-equivalence (cf.\ Huet and Miller).\ + modulo @{text "\\\"}-equivalence (cf.\ Huet and Miller). +\ notepad begin @@ -972,14 +952,10 @@ Combining these characteristics leads to the following general scheme for elimination rules with cases: - \begin{itemize} - \<^item> prefix of assumptions (or ``major premises'') \<^item> one or more cases that enable to establish the main conclusion in an augmented context - - \end{itemize} \ notepad @@ -1015,16 +991,12 @@ Isar provides some infrastructure to support this: - \begin{itemize} - \<^item> native language elements to state eliminations \<^item> symbolic case names \<^item> method @{method cases} to recover this structure in a sub-proof - - \end{itemize} \ print_statement exE diff -r 3e21699bb83b -r 987533262fc2 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/JEdit/JEdit.thy Fri Oct 16 14:53:26 2015 +0200 @@ -18,8 +18,6 @@ components are fit together in order to make this work. The main building blocks are as follows. - \begin{description} - \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It is built around a concept of parallel and asynchronous document processing, which is supported natively by the parallel proof engine that is @@ -52,7 +50,6 @@ plugin for Isabelle, integrated as standalone application for the main operating system platforms: Linux, Windows, Mac OS X. - \end{description} The subtle differences of Isabelle/ML versus Standard ML, Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be @@ -286,8 +283,6 @@ Isabelle/jEdit enables platform-specific look-and-feel by default as follows. - \begin{description} - \<^descr>[Linux:] The platform-independent \emph{Nimbus} is used by default. @@ -311,7 +306,6 @@ full-screen mode for main editor windows. It is advisable to have the \emph{MacOSX} plugin enabled all the time on that platform. - \end{description} Users may experiment with different look-and-feels, but need to keep in mind that this extra variance of GUI functionality is unlikely to @@ -349,8 +343,6 @@ The Isabelle/jEdit \textbf{application} and its plugins provide various font properties that are summarized below. - \begin{itemize} - \<^item> \emph{Global Options / Text Area / Text font}: the main text area font, which is also used as reference point for various derived font sizes, e.g.\ the Output panel (\secref{sec:output}). @@ -372,7 +364,6 @@ \<^item> \emph{Plugin Options / Console / General / Font}: the console window font, e.g.\ relevant for Isabelle/Scala command-line. - \end{itemize} In \figref{fig:isabelle-jedit-hdpi} the \emph{Metal} look-and-feel is configured with custom fonts at 30 pixels, and the main text area and @@ -419,8 +410,6 @@ Compared to plain jEdit, dockable window management in Isabelle/jEdit is slightly augmented according to the the following principles: - \begin{itemize} - \<^item> Floating windows are dependent on the main window as \emph{dialog} in the sense of Java/AWT/Swing. Dialog windows always stay on top of the view, which is particularly important in full-screen mode. The desktop environment @@ -441,8 +430,6 @@ independently of ongoing changes of the PIDE document-model. Note that Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a similar \emph{Detach} operation as an icon. - - \end{itemize} \ @@ -518,8 +505,6 @@ This is a summary for practically relevant input methods for Isabelle symbols. - \begin{enumerate} - \<^enum> The \emph{Symbols} panel: some GUI buttons allow to insert certain symbols in the text buffer. There are also tooltips to reveal the official Isabelle representation with some additional @@ -579,7 +564,6 @@ explicit completion (see also @{verbatim "C+b"} explained in \secref{sec:completion}). - \end{enumerate} \paragraph{Control symbols.} There are some special control symbols to modify the display style of a single symbol (without @@ -753,8 +737,6 @@ \emph{document nodes}. The overall document structure is defined by the theory nodes in two dimensions: - \begin{enumerate} - \<^enum> via \textbf{theory imports} that are specified in the \emph{theory header} using concrete syntax of the @{command_ref theory} command @{cite "isabelle-isar-ref"}; @@ -763,7 +745,6 @@ \emph{load commands}, notably @{command_ref ML_file} and @{command_ref SML_file} @{cite "isabelle-isar-ref"}. - \end{enumerate} In any case, source files are managed by the PIDE infrastructure: the physical file-system only plays a subordinate role. The relevant version of @@ -985,7 +966,6 @@ \<^medskip> The following GUI elements are common to all query modes: - \begin{itemize} \<^item> The spinning wheel provides feedback about the status of a pending query wrt.\ the evaluation of its context and its own operation. @@ -1001,7 +981,6 @@ \<^item> The \emph{Zoom} box controls the font size of the output area. - \end{itemize} All query operations are asynchronous: there is no need to wait for the evaluation of the document for the query context, nor for the query @@ -1154,8 +1133,6 @@ kinds and purposes. The completion mechanism supports this by the following built-in templates: - \begin{description} - \<^descr> @{verbatim "`"} (single ASCII back-quote) supports \emph{quotations} via text cartouches. There are three selections, which are always presented in the same order and do not depend on any context information. The default @@ -1169,7 +1146,6 @@ prefix to let semantic completion of name-space entries propose antiquotation names. - \end{description} With some practice, input of quoted sub-languages and antiquotations of embedded languages should work fluently. Note that national keyboard layouts @@ -1342,8 +1318,6 @@ optional delay after keyboard input according to @{system_option jedit_completion_delay}. - \begin{description} - \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"} with keyboard shortcut @{verbatim "C+b"}. This overrides the shortcut for @{action_ref "complete-word"} in jEdit, but it is @@ -1358,32 +1332,26 @@ \<^descr>[Implicit completion] works via regular keyboard input of the editor. It depends on further side-conditions: - \begin{enumerate} - - \<^enum> The system option @{system_option_ref jedit_completion} needs to - be enabled (default). + \<^enum> The system option @{system_option_ref jedit_completion} needs to + be enabled (default). - \<^enum> Completion of syntax keywords requires at least 3 relevant - characters in the text. - - \<^enum> The system option @{system_option_ref jedit_completion_delay} - determines an additional delay (0.5 by default), before opening a completion - popup. The delay gives the prover a chance to provide semantic completion - information, notably the context (\secref{sec:completion-context}). + \<^enum> Completion of syntax keywords requires at least 3 relevant + characters in the text. - \<^enum> The system option @{system_option_ref jedit_completion_immediate} - (enabled by default) controls whether replacement text should be inserted - immediately without popup, regardless of @{system_option - jedit_completion_delay}. This aggressive mode of completion is restricted to - Isabelle symbols and their abbreviations (\secref{sec:symbols}). + \<^enum> The system option @{system_option_ref jedit_completion_delay} + determines an additional delay (0.5 by default), before opening a completion + popup. The delay gives the prover a chance to provide semantic completion + information, notably the context (\secref{sec:completion-context}). - \<^enum> Completion of symbol abbreviations with only one relevant - character in the text always enforces an explicit popup, - regardless of @{system_option_ref jedit_completion_immediate}. + \<^enum> The system option @{system_option_ref jedit_completion_immediate} + (enabled by default) controls whether replacement text should be inserted + immediately without popup, regardless of @{system_option + jedit_completion_delay}. This aggressive mode of completion is restricted to + Isabelle symbols and their abbreviations (\secref{sec:symbols}). - \end{enumerate} - - \end{description} + \<^enum> Completion of symbol abbreviations with only one relevant + character in the text always enforces an explicit popup, + regardless of @{system_option_ref jedit_completion_immediate}. \ @@ -1434,8 +1402,6 @@ all combinations make sense. At least the following important cases are well-defined: - \begin{description} - \<^descr>[No selection.] The original is removed and the replacement inserted, depending on the caret position. @@ -1448,7 +1414,6 @@ is removed and the replacement is inserted for each line (or segment) of the selection. - \end{description} Support for multiple selections is particularly useful for \emph{HyperSearch}: clicking on one of the items in the \emph{HyperSearch @@ -1473,8 +1438,6 @@ completion. They may be configured in \emph{Plugin Options~/ Isabelle~/ General} as usual. - \begin{itemize} - \<^item> @{system_option_def completion_limit} specifies the maximum number of items for various semantic completion operations (name-space entries etc.) @@ -1520,8 +1483,6 @@ \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated list of markup elements that delimit words in the source that is subject to spell-checking, including various forms of comments. - - \end{itemize} \ @@ -1561,8 +1522,6 @@ \emph{Plugin Options~/ Isabelle~/ General~/ Automatically tried tools}): - \begin{itemize} - \<^item> @{system_option_ref auto_methods} controls automatic use of a combination of standard proof methods (@{method auto}, @{method simp}, @{method blast}, etc.). This corresponds to the Isar command @@ -1603,13 +1562,10 @@ This tool is \emph{enabled} by default. - \end{itemize} Invocation of automatically tried tools is subject to some global policies of parallel execution, which may be configured as follows: - \begin{itemize} - \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the timeout (in seconds) for each tool execution. @@ -1617,7 +1573,6 @@ start delay (in seconds) for automatically tried tools, after the main command evaluation is finished. - \end{itemize} Each tool is submitted independently to the pool of parallel execution tasks in Isabelle/ML, using hardwired priorities according @@ -1782,8 +1737,6 @@ Beyond this, it is occasionally useful to inspect low-level output channels via some of the following additional panels: - \begin{itemize} - \<^item> \emph{Protocol} shows internal messages between the Isabelle/Scala and Isabelle/ML side of the PIDE document editing protocol. Recording of messages starts with the first activation of the @@ -1823,16 +1776,12 @@ Under normal situations, such low-level system output can be ignored. - - \end{itemize} \ chapter \Known problems and workarounds \label{sec:problems}\ text \ - \begin{itemize} - \<^item> \textbf{Problem:} Odd behavior of some diagnostic commands with global side-effects, like writing a physical file. @@ -1899,8 +1848,6 @@ \textbf{Workaround:} Use native full-screen control of the window manager (notably on Mac OS X). - - \end{itemize} \ end \ No newline at end of file diff -r 3e21699bb83b -r 987533262fc2 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/System/Basics.thy Fri Oct 16 14:53:26 2015 +0200 @@ -16,8 +16,6 @@ The Isabelle system environment provides the following basic infrastructure to integrate tools smoothly. - \begin{enumerate} - \<^enum> The \emph{Isabelle settings} mechanism provides process environment variables to all Isabelle executables (including tools and user interfaces). @@ -32,8 +30,6 @@ isabelle}) provides a generic startup environment Isabelle related utilities, user interfaces etc. Such tools automatically benefit from the settings mechanism. - - \end{enumerate} \ @@ -72,8 +68,6 @@ process tree, i.e.\ the environment is passed to subprocesses according to regular Unix conventions. - \begin{enumerate} - \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined automatically from the location of the binary that has been run. @@ -106,8 +100,7 @@ Typically, a user settings file contains only a few lines, with some assignments that are actually changed. Never copy the central @{file "$ISABELLE_HOME/etc/settings"} file! - - \end{enumerate} + Since settings files are regular GNU @{executable_def bash} scripts, one may use complex shell commands, such as @{verbatim "if"} or @@ -120,8 +113,6 @@ \<^medskip> A few variables are somewhat special: - \begin{itemize} - \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set automatically to the absolute path names of the @{executable "isabelle_process"} and @{executable isabelle} executables, @@ -132,7 +123,6 @@ the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically to its value. - \end{itemize} \<^medskip> Note that the settings environment may be inspected with @@ -148,8 +138,6 @@ may add their own selection. Variables that are special in some sense are marked with @{text "\<^sup>*"}. - \begin{description} - \<^descr>[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform user home directory. On Unix systems this is usually the same as @{setting HOME}, but on Windows it is the regular home directory of @@ -276,8 +264,6 @@ \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the prefix from which any running @{executable "isabelle_process"} derives an individual directory for temporary files. - - \end{description} \ @@ -288,8 +274,6 @@ Isabelle distribution itself, and the following two files (both optional) have a special meaning: - \begin{itemize} - \<^item> @{verbatim "etc/settings"} holds additional settings that are initialized when bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As usual, the content is interpreted as a @@ -311,7 +295,6 @@ given here can be either absolute (with leading @{verbatim "/"}) or relative to the component's main directory. - \end{itemize} The root of component initialization is @{setting ISABELLE_HOME} itself. After initializing all of its sub-components recursively, diff -r 3e21699bb83b -r 987533262fc2 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/System/Misc.thy Fri Oct 16 14:53:26 2015 +0200 @@ -75,8 +75,6 @@ We describe the usage of the directory browser and the meaning of the different items in the browser window. - \begin{itemize} - \<^item> A red arrow before a directory name indicates that the directory is currently ``folded'', i.e.~the nodes in this directory are collapsed to one single node. In the right sub-window, the names @@ -95,8 +93,6 @@ focuses to the corresponding node. Double clicking invokes a text viewer window in which the contents of the theory file are displayed. - - \end{itemize} \ @@ -124,8 +120,6 @@ in the full application version. The meaning of the menu items is as follows: - \begin{description} - \<^descr>[Open \dots] Open a new graph file. \<^descr>[Export to PostScript] Outputs the current graph in Postscript @@ -137,8 +131,6 @@ documents. \<^descr>[Quit] Quit the graph browser. - - \end{description} \ @@ -156,8 +148,6 @@ The meaning of the items in a vertex description is as follows: - \begin{description} - \<^descr>[@{text vertex_name}] The name of the vertex. \<^descr>[@{text vertex_ID}] The vertex identifier. Note that there may @@ -177,8 +167,6 @@ ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the browser assumes that successor nodes are listed. - - \end{description} \ @@ -449,8 +437,6 @@ to the much simpler and more efficient YXML format of Isabelle (stdout). The YXML format is defined as follows. - \begin{enumerate} - \<^enum> The encoding is always UTF-8. \<^enum> Body text is represented verbatim (no escaping, no special @@ -472,7 +458,6 @@ @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in well-formed XML documents. - \end{enumerate} Parsing YXML is pretty straight-forward: split the text into chunks separated by @{text "\<^bold>X"}, then split each chunk into diff -r 3e21699bb83b -r 987533262fc2 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/System/Sessions.thy Fri Oct 16 14:53:26 2015 +0200 @@ -77,8 +77,6 @@ document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) \} - \begin{description} - \<^descr> \isakeyword{session}~@{text "A = B + body"} defines a new session @{text "A"} based on parent session @{text "B"}, with its content given in @{text body} (theories and auxiliary source files). @@ -142,8 +140,6 @@ \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text "document) files"}, i.e.\ document sources are taken from the base directory @{verbatim document} within the session root directory. - - \end{description} \ @@ -169,8 +165,6 @@ sessions, in particular with document preparation (\chref{ch:present}). - \begin{itemize} - \<^item> @{system_option_def "browser_info"} controls output of HTML browser info, see also \secref{sec:info}. @@ -229,7 +223,6 @@ processes that get out of control, even if there is a deadlock without CPU time usage. - \end{itemize} The @{tool_def options} tool prints Isabelle system options. Its command-line usage is: diff -r 3e21699bb83b -r 987533262fc2 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Oct 16 14:53:26 2015 +0200 @@ -204,7 +204,6 @@ in if Toplevel.is_skipped_proof state then "" else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms - andalso false (* FIXME *) then let val ants = Antiquote.read' pos syms;