diff -r 151f894984d8 -r 2bf52eec4e8a src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Wed Oct 14 15:06:42 2015 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Wed Oct 14 15:10:32 2015 +0200 @@ -74,7 +74,7 @@ \begin{description} - \item @{command "theory"}~@{text "A \ B\<^sub>1 \ B\<^sub>n \"} + \<^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 than one ancestor, the resulting theory structure of an Isabelle @@ -104,13 +104,13 @@ It is possible to specify an alternative completion via @{verbatim "=="}~@{text "text"}, while the default is the corresponding keyword name. - \item @{command (global) "end"} concludes the current theory + \<^descr> @{command (global) "end"} concludes the current theory definition. Note that some other commands, e.g.\ local theory targets @{command locale} or @{command class} may involve a @{keyword "begin"} that needs to be matched by @{command (local) "end"}, according to the usual rules for nested blocks. - \item @{command thy_deps} visualizes the theory hierarchy as a directed + \<^descr> @{command thy_deps} visualizes the theory hierarchy as a directed acyclic graph. By default, all imported theories are shown, taking the base session as a starting point. Alternatively, it is possibly to restrict the full theory graph by giving bounds, analogously to @@ -155,13 +155,13 @@ \begin{description} - \item @{command "context"}~@{text "c \"} opens a named + \<^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 @{keyword "begin"} keyword as well, in order to continue the local theory immediately after the initial specification. - \item @{command "context"}~@{text "bundles elements \"} opens + \<^descr> @{command "context"}~@{text "bundles elements \"} opens an unnamed context, by extending the enclosing global or local theory target by the given declaration bundles (\secref{sec:bundle}) and context elements (@{text "\"}, @{text "\"} @@ -169,12 +169,12 @@ in the extended context will be exported into the enclosing target by lifting over extra parameters and premises. - \item @{command (local) "end"} concludes the current local theory, + \<^descr> @{command (local) "end"} concludes the current local theory, according to the nesting of contexts. Note that a global @{command (global) "end"} has a different meaning: it concludes the theory itself (\secref{sec:begin-thy}). - \item @{keyword "private"} or @{keyword "qualified"} may be given as + \<^descr> @{keyword "private"} or @{keyword "qualified"} may be given as modifiers before any local theory command. This restricts name space accesses to the local scope, as determined by the enclosing @{command "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its @@ -185,7 +185,7 @@ a local scope by itself: an extra unnamed context is required to use @{keyword "private"} or @{keyword "qualified"} here. - \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local + \<^descr> @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local theory command specifies an immediate target, e.g.\ ``@{command "definition"}~@{text "(\ c)"}'' or ``@{command "theorem"}~@{text "(\ c)"}''. This works both in a local or global theory context; the @@ -258,28 +258,28 @@ \begin{description} - \item @{command bundle}~@{text "b = decls"} defines a bundle of + \<^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 targets are subject to transformations via morphisms, when moved into different application contexts; this works analogously to any other local theory specification. - \item @{command print_bundles} prints the named bundles that are available + \<^descr> @{command print_bundles} prints the named bundles that are available in the current context; the ``@{text "!"}'' option indicates extra verbosity. - \item @{command include}~@{text "b\<^sub>1 \ b\<^sub>n"} includes the declarations + \<^descr> @{command include}~@{text "b\<^sub>1 \ b\<^sub>n"} includes the declarations from the given bundles into the current proof body context. This is analogous to @{command "note"} (\secref{sec:proof-facts}) with the expanded bundles. - \item @{command including} is similar to @{command include}, but + \<^descr> @{command including} is similar to @{command include}, but works in proof refinement (backward mode). This is analogous to @{command "using"} (\secref{sec:proof-facts}) with the expanded bundles. - \item @{keyword "includes"}~@{text "b\<^sub>1 \ b\<^sub>n"} is similar to + \<^descr> @{keyword "includes"}~@{text "b\<^sub>1 \ b\<^sub>n"} is similar to @{command include}, but works in situations where a specification context is constructed, notably for @{command context} and long statements of @{command theorem} etc. @@ -326,7 +326,7 @@ \begin{description} - \item @{command "definition"}~@{text "c \ eq"} produces an + \<^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 given proposition may deviate from internal meta-level equality @@ -340,10 +340,10 @@ @{text "f \ \x y. t"} and @{text "y \ 0 \ g x y = u"} instead of an unrestricted @{text "g \ \x y. u"}. - \item @{command "print_defn_rules"} prints the definitional rewrite rules + \<^descr> @{command "print_defn_rules"} prints the definitional rewrite rules declared via @{attribute defn} in the current context. - \item @{command "abbreviation"}~@{text "c \ eq"} introduces a + \<^descr> @{command "abbreviation"}~@{text "c \ eq"} introduces a syntactic constant which is associated with a certain term according to the meta-level equality @{text eq}. @@ -360,7 +360,7 @@ declared for abbreviations, cf.\ @{command "syntax"} in \secref{sec:syn-trans}. - \item @{command "print_abbrevs"} prints all constant abbreviations of the + \<^descr> @{command "print_abbrevs"} prints all constant abbreviations of the current context; the ``@{text "!"}'' option indicates extra verbosity. \end{description} @@ -382,7 +382,7 @@ \begin{description} - \item @{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m \ \\<^sub>1 \ \\<^sub>n"} + \<^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 for all, which prevents additional specifications for the same constants @@ -432,7 +432,7 @@ \begin{description} - \item @{command "declaration"}~@{text d} adds the declaration + \<^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 function is transformed according to the morphisms being involved in @@ -442,11 +442,11 @@ declaration is applied to all possible contexts involved, including the global background theory. - \item @{command "syntax_declaration"} is similar to @{command + \<^descr> @{command "syntax_declaration"} is similar to @{command "declaration"}, but is meant to affect only ``syntactic'' tools by convention (such as notation and type-checking information). - \item @{command "declare"}~@{text thms} declares theorems to the + \<^descr> @{command "declare"}~@{text thms} declares theorems to the current local theory context. No theorem binding is involved here, unlike @{command "lemmas"} (cf.\ \secref{sec:theorems}), so @{command "declare"} only has the effect of applying attributes as @@ -565,7 +565,7 @@ \begin{description} - \item @{command "locale"}~@{text "loc = import + body"} defines a + \<^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 (@{text body}). Both @{text import} and @{text body} are optional; @@ -590,29 +590,29 @@ \begin{description} - \item @{element "fixes"}~@{text "x :: \ (mx)"} declares a local + \<^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 "constrains"}~@{text "x :: \"} introduces a type + \<^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 "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"} + \<^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 "defines"}~@{text "a: x \ t"} defines a previously + \<^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 "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} + \<^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. @@ -649,25 +649,25 @@ \secref{sec:object-logic}). Separate introduction rules @{text loc_axioms.intro} and @{text loc.intro} are provided as well. - \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an + \<^descr> @{command experiment}~@{text exprs}~@{keyword "begin"} opens an anonymous locale context with private naming policy. Specifications in its body are inaccessible from outside. This is useful to perform experiments, without polluting the name space. - \item @{command "print_locale"}~@{text "locale"} prints the + \<^descr> @{command "print_locale"}~@{text "locale"} prints the contents of the named locale. The command omits @{element "notes"} elements by default. Use @{command "print_locale"}@{text "!"} to have them included. - \item @{command "print_locales"} prints the names of all locales of the + \<^descr> @{command "print_locales"} prints the names of all locales of the current theory; the ``@{text "!"}'' option indicates extra verbosity. - \item @{command "locale_deps"} visualizes all locales and their + \<^descr> @{command "locale_deps"} visualizes all locales and their relations as a Hasse diagram. This includes locales defined as type classes (\secref{sec:class}). See also @{command "print_dependencies"} below. - \item @{method intro_locales} and @{method unfold_locales} + \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all introduction rules of locale predicates of the theory. While @{method intro_locales} only applies the @{text loc.intro} introduction rules and therefore does not descend to @@ -718,7 +718,7 @@ \begin{description} - \item @{command "interpretation"}~@{text "expr \ eqns"} + \<^descr> @{command "interpretation"}~@{text "expr \ eqns"} interprets @{text expr} in a global or local theory. The command generates proof obligations for the instantiated specifications. Once these are discharged by the user, instantiated declarations (in @@ -759,13 +759,13 @@ concepts introduced through definitions. The equations must be proved. - \item @{command "interpret"}~@{text "expr \ eqns"} interprets + \<^descr> @{command "interpret"}~@{text "expr \ eqns"} interprets @{text expr} in the proof context and is otherwise similar to interpretation in local theories. Note that for @{command "interpret"} the @{text eqns} should be explicitly universally quantified. - \item @{command "sublocale"}~@{text "name \ expr \ + \<^descr> @{command "sublocale"}~@{text "name \ expr \ eqns"} interprets @{text expr} in the locale @{text name}. A proof that the specification of @{text name} implies the specification of @@ -798,7 +798,7 @@ be used, but the locale argument must be omitted. The command then refers to the locale (or class) target of the context block. - \item @{command "print_dependencies"}~@{text "expr"} is useful for + \<^descr> @{command "print_dependencies"}~@{text "expr"} is useful for understanding the effect of an interpretation of @{text "expr"} in the current context. It lists all locale instances for which interpretations would be added to the current context. Variant @@ -808,7 +808,7 @@ latter is useful for understanding the dependencies of a locale expression. - \item @{command "print_interps"}~@{text "locale"} lists all + \<^descr> @{command "print_interps"}~@{text "locale"} lists all interpretations of @{text "locale"} in the current theory or proof context, including those due to a combination of an @{command "interpretation"} or @{command "interpret"} and one or several @@ -874,7 +874,7 @@ \begin{description} - \item @{command "permanent_interpretation"}~@{text "expr \ defs \ eqns"} + \<^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. Instantiated declarations (in particular, facts) are added to the @@ -972,7 +972,7 @@ \begin{description} - \item @{command "class"}~@{text "c = superclasses + body"} defines + \<^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 superclasses}. @@ -990,7 +990,7 @@ --- the @{method intro_classes} method takes care of the details of class membership proofs. - \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n)s + \<^descr> @{command "instantiation"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n)s \"} opens a target (cf.\ \secref{sec:target}) which allows to specify class operations @{text "f\<^sub>1, \, f\<^sub>n"} corresponding to sort @{text s} at the particular type instance @{text "(\\<^sub>1 :: s\<^sub>1, @@ -1002,7 +1002,7 @@ this corresponds nicely to mutually recursive type definitions, e.g.\ in Isabelle/HOL. - \item @{command "instance"} in an instantiation target body sets + \<^descr> @{command "instance"} in an instantiation target body sets up a goal stating the type arities claimed at the opening @{command "instantiation"}. The proof would usually proceed by @{method intro_classes}, and then establish the characteristic theorems of @@ -1014,7 +1014,7 @@ need to specify operations: one can continue with the instantiation proof immediately. - \item @{command "subclass"}~@{text c} in a class context for class + \<^descr> @{command "subclass"}~@{text c} in a class context for class @{text d} sets up a goal stating that class @{text c} is logically contained in class @{text d}. After finishing the proof, class @{text d} is proven to be subclass @{text c} and the locale @{text @@ -1027,10 +1027,10 @@ the logical connection are not sufficient on the locale level but on the theory level. - \item @{command "print_classes"} prints all classes in the current + \<^descr> @{command "print_classes"} prints all classes in the current theory. - \item @{command "class_deps"} visualizes classes and their subclass + \<^descr> @{command "class_deps"} visualizes classes and their subclass relations as a directed acyclic graph. By default, all classes from the current theory context are show. This may be restricted by optional bounds as follows: @{command "class_deps"}~@{text upper} or @{command @@ -1038,7 +1038,7 @@ subclass of some sort from @{text upper} and a superclass of some sort from @{text lower}. - \item @{method intro_classes} repeatedly expands all class + \<^descr> @{method intro_classes} repeatedly expands all class introduction rules of this theory. Note that this method usually needs not be named explicitly, as it is already included in the default proof step (e.g.\ of @{command "proof"}). In particular, @@ -1143,7 +1143,7 @@ \begin{description} - \item @{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"} + \<^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 by an explicitly given mapping from variable names @{text "x\<^sub>i"} to @@ -1194,7 +1194,7 @@ \begin{description} - \item @{command "SML_file"}~@{text "name"} reads and evaluates the + \<^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 Standard ML implementation of Poly/ML, without the many add-ons of @@ -1202,41 +1202,41 @@ build larger Standard ML projects, independently of the regular Isabelle/ML environment. - \item @{command "ML_file"}~@{text "name"} reads and evaluates the + \<^descr> @{command "ML_file"}~@{text "name"} reads and evaluates the given ML file. The current theory context is passed down to the ML toplevel and may be modified, using @{ML "Context.>>"} or derived ML commands. Top-level ML bindings are stored within the (global or local) theory context. - \item @{command "ML"}~@{text "text"} is similar to @{command + \<^descr> @{command "ML"}~@{text "text"} is similar to @{command "ML_file"}, but evaluates directly the given @{text "text"}. Top-level ML bindings are stored within the (global or local) theory context. - \item @{command "ML_prf"} is analogous to @{command "ML"} but works + \<^descr> @{command "ML_prf"} is analogous to @{command "ML"} but works within a proof context. Top-level ML bindings are stored within the proof context in a purely sequential fashion, disregarding the nested proof structure. ML bindings introduced by @{command "ML_prf"} are discarded at the end of the proof. - \item @{command "ML_val"} and @{command "ML_command"} are diagnostic + \<^descr> @{command "ML_val"} and @{command "ML_command"} are diagnostic versions of @{command "ML"}, which means that the context may not be updated. @{command "ML_val"} echos the bindings produced at the ML toplevel, but @{command "ML_command"} is silent. - \item @{command "setup"}~@{text "text"} changes the current theory + \<^descr> @{command "setup"}~@{text "text"} changes the current theory context by applying @{text "text"}, which refers to an ML expression of type @{ML_type "theory -> theory"}. This enables to initialize any object-logic specific tools and packages written in ML, for example. - \item @{command "local_setup"} is similar to @{command "setup"} for + \<^descr> @{command "local_setup"} is similar to @{command "setup"} for a local theory context, and an ML expression of type @{ML_type "local_theory -> local_theory"}. This allows to invoke local theory specification packages without going through concrete outer syntax, for example. - \item @{command "attribute_setup"}~@{text "name = text description"} + \<^descr> @{command "attribute_setup"}~@{text "name = text description"} defines an attribute in the current context. The given @{text "text"} has to be an ML expression of type @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in @@ -1268,16 +1268,16 @@ text \ \begin{description} - \item @{attribute ML_print_depth} controls the printing depth of the ML + \<^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 such as 100--1000 are occasionally useful for debugging. - \item @{attribute ML_source_trace} indicates whether the source text that + \<^descr> @{attribute ML_source_trace} indicates whether the source text that is given to the ML compiler should be output: it shows the raw Standard ML after expansion of Isabelle/ML antiquotations. - \item @{attribute ML_exception_trace} indicates whether the ML run-time + \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system should print a detailed stack trace on exceptions. The result is dependent on the particular ML compiler version. Note that after Poly/ML 5.3 some optimizations in the run-time systems may hinder exception @@ -1308,7 +1308,7 @@ \begin{description} - \item @{command "default_sort"}~@{text s} makes sort @{text s} the + \<^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). Type variables generated by type inference are not affected. @@ -1341,13 +1341,13 @@ \begin{description} - \item @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces a + \<^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 are merely syntactic abbreviations without any logical significance. Internally, type synonyms are fully expanded. - \item @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} declares a new + \<^descr> @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} declares a new type constructor @{text t}. If the object-logic defines a base sort @{text s}, then the constructor is declared to operate on that, via the axiomatic type-class instance @{text "t :: (s, \, s)s"}. @@ -1424,12 +1424,12 @@ \begin{description} - \item @{command "consts"}~@{text "c :: \"} declares constant @{text + \<^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 declared. - \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn} + \<^descr> @{command "defs"}~@{text "name: eqn"} introduces @{text eqn} as a definitional axiom for some existing constant. The @{text "(unchecked)"} option disables global dependency checks @@ -1463,13 +1463,13 @@ \begin{description} - \item @{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}~@{keyword_def + \<^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. Results are standardized before being stored, i.e.\ schematic variables are renamed to enforce index @{text "0"} uniformly. - \item @{command "named_theorems"}~@{text "name description"} declares a + \<^descr> @{command "named_theorems"}~@{text "name description"} declares a dynamic fact within the context. The same @{text name} is used to define an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the content incrementally, in @@ -1507,7 +1507,7 @@ \begin{description} - \item @{command "oracle"}~@{text "name = text"} turns the given ML + \<^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 global identifier @{ML_text name}. This acts like an infinitary @@ -1545,7 +1545,7 @@ \begin{description} - \item @{command "hide_class"}~@{text names} fully removes class + \<^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. @@ -1554,7 +1554,7 @@ longer accessible to the user are printed with the special qualifier ``@{text "??"}'' prefixed to the full internal name. - \item @{command "hide_type"}, @{command "hide_const"}, and @{command + \<^descr> @{command "hide_type"}, @{command "hide_const"}, and @{command "hide_fact"} are similar to @{command "hide_class"}, but hide types, constants, and facts, respectively.