--- 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 \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
+ \<^descr> @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
starts a new theory @{text A} based on the merge of existing
theories @{text "B\<^sub>1 \<dots> 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 \<BEGIN>"} opens a named
+ \<^descr> @{command "context"}~@{text "c \<BEGIN>"} 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 \<BEGIN>"} opens
+ \<^descr> @{command "context"}~@{text "bundles elements \<BEGIN>"} 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 "\<FIXES>"}, @{text "\<ASSUMES>"}
@@ -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 "(\<IN> c)"}'' or ``@{command "theorem"}~@{text
"(\<IN> 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 \<dots> b\<^sub>n"} includes the declarations
+ \<^descr> @{command include}~@{text "b\<^sub>1 \<dots> 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 \<dots> b\<^sub>n"} is similar to
+ \<^descr> @{keyword "includes"}~@{text "b\<^sub>1 \<dots> 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 \<WHERE> eq"} produces an
+ \<^descr> @{command "definition"}~@{text "c \<WHERE> eq"} produces an
internal definition @{text "c \<equiv> 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 \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
unrestricted @{text "g \<equiv> \<lambda>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 \<WHERE> eq"} introduces a
+ \<^descr> @{command "abbreviation"}~@{text "c \<WHERE> 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 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
+ \<^descr> @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^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 :: \<tau> (mx)"} declares a local
+ \<^descr> @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
parameter of type @{text \<tau>} 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 :: \<tau>"} introduces a type
+ \<^descr> @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
constraint @{text \<tau>} 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: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
+ \<^descr> @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
introduces local premises, similar to @{command "assume"} within a
proof (cf.\ \secref{sec:proof-context}).
- \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
+ \<^descr> @{element "defines"}~@{text "a: x \<equiv> 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 \<dots> x\<^sub>n \<equiv> t"}''.
- \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
+ \<^descr> @{element "notes"}~@{text "a = b\<^sub>1 \<dots> 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 \<WHERE> eqns"}
+ \<^descr> @{command "interpretation"}~@{text "expr \<WHERE> 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 \<WHERE> eqns"} interprets
+ \<^descr> @{command "interpret"}~@{text "expr \<WHERE> 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 \<subseteq> expr \<WHERE>
+ \<^descr> @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
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 \<DEFINING> defs \<WHERE> eqns"}
+ \<^descr> @{command "permanent_interpretation"}~@{text "expr \<DEFINING> defs \<WHERE> 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, \<dots>, s\<^sub>n)s
+ \<^descr> @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
\<BEGIN>"} opens a target (cf.\ \secref{sec:target}) which
allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
to sort @{text s} at the particular type instance @{text "(\<alpha>\<^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 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}
+ \<^descr> @{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}
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 \<open>
\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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
+ \<^descr> @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
\emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type @{text
"\<tau>"}. 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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
+ \<^descr> @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^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, \<dots>, s)s"}.
@@ -1424,12 +1424,12 @@
\begin{description}
- \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
+ \<^descr> @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
c} to have any instance of type scheme @{text \<sigma>}. 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 \<dots> b\<^sub>n"}~@{keyword_def
+ \<^descr> @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def
"for"}~@{text "x\<^sub>1 \<dots> 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.