--- 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}
\<close>
end
--- 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}
\<close>
text %mlantiq \<open>
@@ -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}
\<close>
@@ -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}
\<close>
text %mlex \<open>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}
\<close>
end
--- 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 \<open>\S2\<close> "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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
text %mlex \<open>The following example peeks at a certain goal configuration.\<close>
@@ -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}
\<close>
text %mlex \<open>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}
\<close>
text %mlantiq \<open>
@@ -574,16 +548,12 @@
@@{ML_antiquotation attributes} attributes
\<close>}
- \begin{description}
-
\<^descr> @{text "@{attributes [\<dots>]}"} 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}
\<close>
text %mlex \<open>See also @{command attribute_setup} in
--- 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}
\<close>
--- 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 "(\<kappa>, \<^vec>s, s)"} declares
the arity @{text "\<kappa> :: (\<^vec>s)s"}.
-
- \end{description}
\<close>
text %mlantiq \<open>
@@ -211,8 +207,6 @@
@@{ML_antiquotation typ} type
\<close>}
- \begin{description}
-
\<^descr> @{text "@{class c}"} inlines the internalized class @{text
"c"} --- as @{ML_type string} literal.
@@ -231,8 +225,6 @@
\<^descr> @{text "@{typ \<tau>}"} inlines the internalized type @{text "\<tau>"}
--- as constructor term for datatype @{ML_type typ}.
-
- \end{description}
\<close>
@@ -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, [\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n])"}
convert between two representations of polymorphic constants: full
type instance vs.\ compact type arguments form.
-
- \end{description}
\<close>
text %mlantiq \<open>
@@ -464,8 +452,6 @@
@@{ML_antiquotation prop} prop
\<close>}
- \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 \<phi>}"} inlines the internalized proposition
@{text "\<phi>"} --- as constructor term for datatype @{ML_type term}.
-
- \end{description}
\<close>
@@ -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>\<tau>"}, relative to existing specifications for constants @{text
"\<^vec>d\<^sub>\<sigma>"}. This also works for type constructors.
-
- \end{description}
\<close>
@@ -808,8 +788,6 @@
@'by' method method?
\<close>}
- \begin{description}
-
\<^descr> @{text "@{ctyp \<tau>}"} 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}
-
\<close>
@@ -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(\<tau>)"} recovers the type
@{text "\<tau>"}.
-
- \end{description}
\<close>
@@ -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}
\<close>
text %mlex \<open>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 \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> 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 @@
\<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
Note that this representation looses information about the order of
parameters, and vacuous quantifiers vanish automatically.
-
- \end{itemize}
\<close>
text %mlref \<open>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
text %mlex \<open>Detailed proof information of a theorem may be retrieved
--- 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]
+\<open> (*** section ***)
(** subsection **)
@@ -88,8 +88,7 @@
(*
long paragraph,
with more text
- *)
- \end{verbatim}
+ *)\<close>}
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]
+\<open> (* 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;\<close>}
\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] \<open> fun my_tac ctxt arg1 arg2 i st = ...\<close>}
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}
\<close>
@@ -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]
+\<open> val x = y + z * (a + b);
val pair = (a, b);
- val record = {foo = 1, bar = 2};
- \end{verbatim}
+ val record = {foo = 1, bar = 2};\<close>}
Lines are normally broken \emph{after} an infix operator or
punctuation character. For example:
- \begin{verbatim}
+ @{verbatim [display]
+\<open>
val x =
a +
b +
@@ -326,7 +318,7 @@
(a,
b,
c);
- \end{verbatim}
+\<close>}
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]
+\<open> (* 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\<close>}
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]
+\<open> (* RIGHT *)
fun foo p1 =
expr1
@@ -409,16 +400,15 @@
fun foo p1 =
expr1
| foo p2 =
- expr2
- \end{verbatim}
+ expr2\<close>}
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]
+\<open> (* RIGHT *)
fun foo p1 =
(case e of
@@ -442,8 +432,7 @@
...
in
...
- end
- \end{verbatim}
+ end\<close>}
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]
+\<open> (* RIGHT *)
if b1 then e1
else if b2 then e2
- else e3
- \end{verbatim}
+ else e3\<close>}
\<^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]
+\<open> (* RIGHT *)
fun foo x y = fold (fn z =>
- expr)
- \end{verbatim}
+ expr)\<close>}
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]
+\<open> (* WRONG *)
fun foo x = let
val y = ...
@@ -515,8 +499,7 @@
let
val y = ...
in
- ... end
- \end{verbatim}
+ ... end\<close>}
\<^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}?
\<close>}
- \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}
\<close>
text %mlex \<open>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}
\<close>
text %mlantiq \<open>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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 \<alpha>}'' 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}
\<close>
text %mlex \<open>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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
text %mlex \<open>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}
\<close>
text %mlref \<open>
@@ -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}
\<close>
text %mlex \<open>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}
\<close>
@@ -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, \<dots>, x\<^sub>n]"} is like @{ML
"map"}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"}, but the evaluation of @{text "f x\<^sub>i"}
for @{text "i = 1, \<dots>, 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}
\<close>
text %mlex \<open>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}
\<close>
@@ -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}
\<close>
end
--- 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 "\<Gamma> \<turnstile>\<^sub>\<Theta>
\<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'
@@ -39,7 +37,6 @@
@{text "\<Delta> = \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here,
only the @{text "\<Gamma>"} 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}
\<close>
text %mlantiq \<open>
@@ -167,8 +160,6 @@
@@{ML_antiquotation theory_context} nameref
\<close>}
- \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}
\<close>
@@ -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}
\<close>
text %mlantiq \<open>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
text %mlex \<open>
@@ -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}
\<close>
text %mlex \<open>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}
\<close>
@@ -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}
\<close>
text %mlex \<open>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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
text %mlantiq \<open>
@@ -1039,14 +984,10 @@
@@{ML_antiquotation binding} name
\<close>}
- \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}
\<close>
text %mlex \<open>The following example yields the source position of some
--- 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
"\<And>"} prefix of proposition @{text "B"}, using the given name bindings.
-
- \end{description}
\<close>
text %mlex \<open>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}
\<close>
text %mlex \<open>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}
\<close>
text %mlex \<open>The following minimal example illustrates how to access
--- 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.
--- 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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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 "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, 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}
\<close>
@@ -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 "\<infinity>"}).
-
- \end{description}
\<close>
text %mlex \<open>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}
\<close>
ML \<open>
@@ -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 "\<dots>"}~@{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 "\<dots>"}~@{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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
end
--- 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}
\<close>}
- \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 "\<dots>"}~@{verbatim "*)"} nor verbatim
text @{verbatim "{*"}~@{text "\<dots>"}~@{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 \<open>\nocite{foobar}\<close>}.
-
- \end{description}
\<close>
@@ -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 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
-
- \end{description}
\<close>
@@ -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.\<close>
+ @{verbatim "ROOT"} file.
+\<close>
section \<open>Markup via command tags \label{sec:tags}\<close>
@@ -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 \<open>()\<close>}
@@ -574,8 +559,6 @@
\<^item> Strict repetition with separator @{verbatim "A + sep"}
@{rail \<open>A + sep\<close>}
-
- \end{itemize}
\<close>
@@ -590,14 +573,10 @@
@@{command display_drafts} (@{syntax name} +)
\<close>}
- \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}
\<close>
end
--- 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}))?
\<close>}
- \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}
\<close>
@@ -83,8 +79,6 @@
@@{method sleep} @{syntax real}
\<close>}
- \begin{description}
-
\<^descr> @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
"a\<^sub>1 \<dots> 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}?
\<close>}
- \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}
\<close>
@@ -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}
\<close>
@@ -305,8 +290,6 @@
'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
\<close>}
- \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} ('!'?)
\<close>}
- \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 "\<lambda>"}-abstractions or functional variables.
- For example:
+ \item First-order patterns, considering the sublanguage of
+ application of constant operators to variable operands, without
+ @{text "\<lambda>"}-abstractions or functional variables.
+ For example:
- @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
- @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
+ @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
+ @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
- \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
- These are terms in @{text "\<beta>"}-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 \<dots> 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 "\<beta>"}-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 \<dots> x\<^sub>n"}, where the
+ @{text "x\<^sub>i"} are distinct bound variables.
- For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"}
- or its symmetric form, since the @{text "rhs"} is also a
- higher-order pattern.
+ For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>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 "\<lambda>"}-term
- structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
- variables are treated like quasi-constant term material.
+ \item Physical first-order patterns over raw @{text "\<lambda>"}-term
+ structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
+ variables are treated like quasi-constant term material.
- For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the
- term @{text "g a \<in> range g"} to @{text "True"}, but will fail to
- match @{text "g (h b) \<in> range (\<lambda>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 \<Longrightarrow> ?y \<in> 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 \<in> range ?f = True"} rewrites the
+ term @{text "g a \<in> range g"} to @{text "True"}, but will fail to
+ match @{text "g (h b) \<in> range (\<lambda>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 \<Longrightarrow> ?y \<in> 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}
\<close>
(*<*)experiment begin(*>*)
@@ -866,8 +838,6 @@
@@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
\<close>}
- \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}
\<close>
@@ -944,8 +912,6 @@
rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow>
?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:
\<close>
@@ -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') ')'
\<close>}
- \begin{description}
-
\<^descr> @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,
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}
\<close>
@@ -1436,8 +1391,6 @@
@@{attribute iff} (((() | 'add') '?'?) | 'del')
\<close>}
- \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 @@
"\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for
illustrative purposes: the Classical Reasoner already swaps rules
internally as explained above.
-
- \end{description}
\<close>
@@ -1504,8 +1455,6 @@
@@{method rule} @{syntax thmrefs}?
\<close>}
- \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 "\<not> A"} and @{text A}. Chained
facts, which are guaranteed to participate, may appear in either
order.
-
- \end{description}
\<close>
@@ -1564,8 +1511,6 @@
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
\<close>}
- \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] \<open>Function unknown's argument not a bound variable\<close>}
+ \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] \<open>Function unknown's argument not a bound variable\<close>}
- \<^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} * )
\<close>}
- \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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -1872,8 +1804,6 @@
@@{attribute rule_format} ('(' 'noasm' ')')?
\<close>}
- \begin{description}
-
\<^descr> @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
@{text c} as the truth judgment of the current object-logic. Its
type @{text \<sigma>} should specify a coercion of the category of
@@ -1908,8 +1838,6 @@
rule_format} is to replace (bounded) universal quantification
(@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
-
- \end{description}
\<close>
@@ -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
--- 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')
\<close>}
- \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}
\<close>
@@ -160,8 +156,6 @@
text \<open>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, \<dots>, R\<^sub>n"} are defined simultaneously,
the list of introduction rules is called @{text "R\<^sub>1_\<dots>_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 \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for proving
monotonicity of inductive definitions whose introduction rules have
premises involving terms such as @{text "\<M> R t"}.
@@ -218,8 +209,6 @@
@{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
@{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
\]
-
- \end{itemize}
\<close>
subsubsection \<open>Examples\<close>
@@ -290,8 +279,6 @@
@@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \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}
\<close>
@@ -535,8 +517,6 @@
orders: ( 'max' | 'min' | 'ms' ) *
\<close>}
- \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}
\<close>
@@ -594,8 +572,6 @@
@'where' @{syntax thmdecl}? @{syntax prop}
\<close>}
- \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}
\<close>
@@ -671,8 +645,6 @@
(() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
\<close>}
- \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')
\<close>}
- \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}
\<close>
@@ -758,8 +725,6 @@
decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')?
\<close>}
- \begin{description}
-
\<^descr> @{command (HOL) "specification"}~@{text "decls \<phi>"} 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}
\<close>
@@ -795,15 +758,12 @@
cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
\<close>}
- \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}?
\<close>}
- \begin{description}
-
\<^descr> @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
\<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
derived from the optional parent record @{text "\<tau>"} by adding new
@@ -971,8 +926,6 @@
"(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for
@{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
\<zeta>\<rparr>"}.
-
- \end{description}
\<close>
@@ -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}
\<close>
@@ -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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} defines a
new type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} from the set @{text A} over an existing
type. The set @{text A} may contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^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}
\<close>
@@ -1272,8 +1217,6 @@
@@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
\<close>}
- \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 "\<sigma>\<^sub>1"}, \ldots, @{text "\<sigma>\<^sub>k"} is a subsequence of @{text
"\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1"}, @{text "\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1"}, \ldots, @{text "\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n"}, @{text
"\<beta>\<^sub>n \<Rightarrow> \<alpha>\<^sub>n"}.
-
- \end{description}
\<close>
@@ -1330,8 +1271,6 @@
quot_parametric: @'parametric' @{syntax thmref}
\<close>}
- \begin{description}
-
\<^descr> @{command (HOL) "quotient_type"} defines a new quotient type @{text
\<tau>}. The injection from a quotient type to a raw type is called @{text
rep_\<tau>}, its inverse @{text abs_\<tau>} 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}
\<close>
@@ -1405,33 +1342,31 @@
@{syntax thmref} (@{syntax thmref} @{syntax thmref})?
\<close>}
- \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 "\<tau>"} is a type variable
-
- \<^descr> @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
- where @{text "\<kappa>"} is an abstract type constructor and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"}
- do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
- @{typ "int dlist dlist"} not)
-
- \<^descr> @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} 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 "\<tau>"} is a type variable
+
+ \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
+ where @{text "\<kappa>"} is an abstract type constructor and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"}
+ do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
+ @{typ "int dlist dlist"} not)
+
+ \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} 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}
\<close>
@@ -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}?
\<close>}
- \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 \<Longrightarrow>
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}
\<close>
@@ -1855,8 +1781,6 @@
facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
\<close>} % 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}
\<close>
@@ -1929,8 +1851,6 @@
args: ( @{syntax name} '=' value + ',' )
\<close>} % 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}
\<close>
@@ -2142,8 +2060,6 @@
@@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+)
\<close>}
- \begin{description}
-
\<^descr> @{attribute (HOL) "coercion"}~@{text "f"} registers a new
coercion function @{text "f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2"} where @{text "\<sigma>\<^sub>1"} and
@{text "\<sigma>\<^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}
\<close>
@@ -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} *)
\<close>}
- \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}
\<close>
@@ -2266,8 +2173,6 @@
@{syntax thmrefs}?
\<close>}
- \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}
\<close>
@@ -2299,8 +2202,6 @@
@@{attribute (HOL) algebra} (() | 'add' | 'del')
\<close>}
- \begin{description}
-
\<^descr> @{method (HOL) algebra} performs algebraic reasoning via
Gr\"obner bases, see also @{cite "Chaieb-Wenzel:2007"} and
@{cite \<open>\S3.2\<close> "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 \<noteq> 0"} anywhere within a universal problem statement.
-
- \<^enum> All-exists problems of the following restricted (but useful)
- form:
-
- @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
- e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
- (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
- p\<^sub>1\<^sub>1(x\<^sub>1, \<dots> ,x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>1\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0 \<and>
- \<dots> \<and>
- p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
-
- Here @{text "e\<^sub>1, \<dots>, 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 \<noteq> 0"} anywhere within a universal problem statement.
+
+ \item All-exists problems of the following restricted (but useful)
+ form:
+
+ @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
+ e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
+ (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
+ p\<^sub>1\<^sub>1(x\<^sub>1, \<dots> ,x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>1\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0 \<and>
+ \<dots> \<and>
+ p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
+
+ Here @{text "e\<^sub>1, \<dots>, 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}
\<close>
@@ -2380,14 +2279,10 @@
@@{method (HOL) coherent} @{syntax thmrefs}?
\<close>}
- \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}
\<close>
@@ -2417,8 +2312,6 @@
rule: 'rule' ':' @{syntax thmref}
\<close>}
- \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}
\<close>
-
section \<open>Adhoc tuples\<close>
text \<open>
@@ -2461,16 +2351,12 @@
@@{attribute (HOL) split_format} ('(' 'complete' ')')?
\<close>}
- \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}
\<close>
@@ -2601,8 +2487,6 @@
modes: mode @'as' const
\<close>}
- \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}
\<close>
end
--- 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} + ) ')'
\<close>}
- \begin{description}
-
\<^descr> @{command "typ"}~@{text \<tau>} 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}
\<close>
@@ -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 \<open>""\<close>} (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}
\<close>
@@ -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')
\<close>}
- \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}
\<close>
@@ -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 "(\<dots>)"} 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 "\<lambda>x _. x"}, which is @{text "\<alpha>"}-equivalent to @{text
- "\<lambda>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 "\<lambda>x _. x"}, which is @{text "\<alpha>"}-equivalent to @{text
+ "\<lambda>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}
\<close>
@@ -899,54 +866,50 @@
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\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 "\<dots> => 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 "\<dots> => 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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>}
- \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 "\<tau>\<^sub>i = prop"}
+ \item @{text "prop"} if @{text "\<tau>\<^sub>i = prop"}
- \<^item> @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
- constructor @{text "\<kappa> \<noteq> prop"}
+ \item @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
+ constructor @{text "\<kappa> \<noteq> prop"}
- \<^item> @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
+ \item @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
- \<^item> @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
- (syntactic type constructor)
+ \item @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
+ (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 \<leftarrow> xs . P]"} as defined in theory @{theory
List} in Isabelle/HOL.
+\<close>
- \end{itemize}
-\<close>
subsubsection \<open>Applying translation rules\<close>
@@ -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
\<close>}
- \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}
\<close>
@@ -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
--- 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} * )
\<close>}
- \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}
\<close>
@@ -73,8 +69,6 @@
text \<open>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 "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
@{text "\<open>\<phi>\<close>"} (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}
\<close>
end
--- 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}
\<close>}
- \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}
\<close>
@@ -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}
\<close>
@@ -190,8 +179,6 @@
@{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
\<close>}
- \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}
\<close>
@@ -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 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous
higher-order matching against terms @{text "t\<^sub>1, \<dots>, 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')
\<close>}
- \begin{description}
-
\<^descr> @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
@{text "b\<^sub>1, \<dots>, 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, \<dots> 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')
\<close>}
- \begin{description}
-
\<^descr> @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
@{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
\<phi>"} 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')
\<close>}
- \begin{description}
-
\<^descr> @{command "also"}~@{text "(a\<^sub>1 \<dots> 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}
\<close>
@@ -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})
\<close>}
- \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}
\<close>
@@ -860,8 +825,6 @@
@@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}
\<close>}
- \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 "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
be specified as for @{attribute "of"} above.
-
- \end{description}
\<close>
@@ -986,8 +947,6 @@
@@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
- \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}
\<close>
(*<*)experiment begin(*>*)
@@ -1094,8 +1051,6 @@
@@{attribute consumes} @{syntax int}?
\<close>}
- \begin{description}
-
\<^descr> @{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^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}
\<close>
@@ -1214,8 +1167,6 @@
taking: 'taking' ':' @{syntax insts}
\<close>}
- \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'
\<close>}
- \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}
\<close>
@@ -1470,8 +1416,6 @@
@@{command guess} (@{syntax "fixes"} + @'and')
\<close>}
- \begin{description}
-
\<^descr> @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
| (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} 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
--- 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}
\<close>}
- \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}
\<close>
@@ -103,8 +99,6 @@
params: @'for' '\<dots>'? (('_' | @{syntax name})+)
\<close>}
- \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:
\<close>
@@ -245,8 +238,6 @@
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
\<close>}
-\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}
\<close>
end
\ No newline at end of file
--- 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} + @'|') ')'
\<close>}
- \begin{description}
-
\<^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
@@ -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}
\<close>
@@ -153,8 +149,6 @@
@{syntax_def target}: '(' @'in' @{syntax nameref} ')'
\<close>}
- \begin{description}
-
\<^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
@@ -193,7 +187,6 @@
``@{text "(\<IN> -)"}'' 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}+)
\<close>}
- \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:\<close>
+ options:
+\<close>
(*<*)experiment begin(*>*)
bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
@@ -324,8 +315,6 @@
@@{command print_abbrevs} ('!'?)
\<close>}
- \begin{description}
-
\<^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
@@ -362,8 +351,6 @@
\<^descr> @{command "print_abbrevs"} prints all constant abbreviations of the
current context; the ``@{text "!"}'' option indicates extra verbosity.
-
- \end{description}
\<close>
@@ -380,8 +367,6 @@
specs: (@{syntax thmdecl}? @{syntax props} + @'and')
\<close>}
- \begin{description}
-
\<^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
@@ -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}
\<close>
@@ -430,8 +413,6 @@
@@{command declare} (@{syntax thmrefs} + @'and')
\<close>}
- \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}
\<close>
@@ -563,8 +542,6 @@
@'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
\<close>}
- \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 :: \<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 "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.
- \<^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 "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.
- \<^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 "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}).
- \<^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 "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"}''.
- \<^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.
+ \item @{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.
\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}
\<close>
@@ -716,8 +691,6 @@
equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \begin{description}
-
\<^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.
@@ -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 \<rightarrow> proof(prove)"}
@@ -872,8 +841,6 @@
equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \begin{description}
-
\<^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.
@@ -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}
\<close>
@@ -970,8 +935,6 @@
class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
\<close>}
- \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}
\<close>
@@ -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[\<alpha>]"} referring to the
local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
@@ -1071,8 +1030,6 @@
global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
resolves ambiguities. In rare cases, manual type annotations are
needed.
-
- \end{itemize}
\<close>
@@ -1141,8 +1098,6 @@
spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
\<close>}
- \begin{description}
-
\<^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
@@ -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}
\<close>
@@ -1192,8 +1145,6 @@
@@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
- \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}
\<close>
(*<*)experiment begin(*>*)
@@ -1266,8 +1215,6 @@
(*<*)end(*>*)
text \<open>
- \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}
\<close>
@@ -1306,8 +1251,6 @@
@@{command default_sort} @{syntax sort}
\<close>}
- \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}
\<close>
@@ -1339,8 +1280,6 @@
@@{command typedecl} @{syntax typespec} @{syntax mixfix}?
\<close>}
- \begin{description}
-
\<^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
@@ -1352,7 +1291,6 @@
@{text s}, then the constructor is declared to operate on that, via
the axiomatic type-class instance @{text "t :: (s, \<dots>, 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'? ')'
\<close>}
- \begin{description}
-
\<^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
@@ -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}
\<close>
@@ -1461,8 +1392,6 @@
@@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
\<close>}
- \begin{description}
-
\<^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.
@@ -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}
\<close>
@@ -1505,8 +1432,6 @@
@@{command oracle} @{syntax name} '=' @{syntax text}
\<close>}
- \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}
\<close>
end
--- 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 \<open>Naming conventions\<close>
text \<open>
- \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}
\<close>
@@ -224,8 +220,6 @@
subsection \<open>Special names in Isar proofs\<close>
text \<open>
- \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}
\<close>
notepad
@@ -313,15 +305,11 @@
subsubsection \<open>Notes\<close>
text \<open>
- \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}
\<close>
@@ -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}
\<close>
notepad
@@ -421,7 +406,6 @@
text \<open>
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}
\<close>
lemma
@@ -682,16 +664,14 @@
text \<open>
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 \<lambda>}-terms
- modulo @{text "\<alpha>\<beta>\<eta>"}-equivalence (cf.\ Huet and Miller).\<close>
+ modulo @{text "\<alpha>\<beta>\<eta>"}-equivalence (cf.\ Huet and Miller).
+\<close>
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}
\<close>
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}
\<close>
print_statement exE
--- 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}
\<close>
@@ -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}.
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
text \<open>
- \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}
\<close>
end
\ No newline at end of file
--- 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}
\<close>
@@ -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}
\<close>
@@ -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,
--- 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}
\<close>
@@ -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}
\<close>
@@ -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}
\<close>
@@ -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
--- 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}+)
\<close>}
- \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}
\<close>
@@ -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:
--- 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;