--- a/src/Doc/Implementation/Isar.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Isar.thy Mon Oct 12 20:58:58 2015 +0200
@@ -10,7 +10,7 @@
\begin{enumerate}
- \item Proof \emph{commands} define the primary language of
+ \<^enum> Proof \emph{commands} define the primary language of
transactions of the underlying Isar/VM interpreter. Typical
examples are @{command "fix"}, @{command "assume"}, @{command
"show"}, @{command "proof"}, and @{command "qed"}.
@@ -19,7 +19,7 @@
to expressions of structured proof text, such that both the machine
and the human reader can give it a meaning as formal reasoning.
- \item Proof \emph{methods} define a secondary language of mixed
+ \<^enum> Proof \emph{methods} define a secondary language of mixed
forward-backward refinement steps involving facts and goals.
Typical examples are @{method rule}, @{method unfold}, and @{method
simp}.
@@ -28,7 +28,7 @@
language, say as arguments to @{command "proof"}, @{command "qed"},
or @{command "by"}.
- \item \emph{Attributes} define a tertiary language of small
+ \<^enum> \emph{Attributes} define a tertiary language of small
annotations to theorems being defined or referenced. Attributes can
modify both the context and the theorem.
@@ -191,14 +191,14 @@
\begin{itemize}
- \item Goal addressing is further limited either to operate
+ \<^item> Goal addressing is further limited either to operate
uniformly on \emph{all} subgoals, or specifically on the
\emph{first} subgoal.
Exception: old-style tactic emulations that are embedded into the
method space, e.g.\ @{method rule_tac}.
- \item A non-trivial method always needs to make progress: an
+ \<^item> A non-trivial method always needs to make progress: an
identical follow-up goal state has to be avoided.\footnote{This
enables the user to write method expressions like @{text "meth\<^sup>+"}
without looping, while the trivial do-nothing case can be recovered
@@ -207,13 +207,14 @@
Exception: trivial stuttering steps, such as ``@{method -}'' or
@{method succeed}.
- \item Goal facts passed to the method must not be ignored. If there
+ \<^item> Goal facts passed to the method must not be ignored. If there
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
+ \<^medskip>
+ Syntactically, the language of proof methods appears as
arguments to Isar commands like @{command "by"} or @{command apply}.
User-space additions are reasonably easy by plugging suitable
method-valued parser functions into the framework, using the
@@ -223,14 +224,14 @@
following Isar proof schemes. This is the general form of
structured proof text:
- \medskip
+ \<^medskip>
\begin{tabular}{l}
@{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\
@{command proof}~@{text "(initial_method)"} \\
\quad@{text "body"} \\
@{command qed}~@{text "(terminal_method)"} \\
\end{tabular}
- \medskip
+ \<^medskip>
The goal configuration consists of @{text "facts\<^sub>1"} and
@{text "facts\<^sub>2"} appended in that order, and various @{text
@@ -240,9 +241,10 @@
"terminal_method"} has another chance to finish any remaining
subgoals, but it does not see the facts of the initial step.
- \medskip This pattern illustrates unstructured proof scripts:
+ \<^medskip>
+ This pattern illustrates unstructured proof scripts:
- \medskip
+ \<^medskip>
\begin{tabular}{l}
@{command have}~@{text "props"} \\
\quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\
@@ -250,7 +252,7 @@
\quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\
\quad@{command done} \\
\end{tabular}
- \medskip
+ \<^medskip>
The @{text "method\<^sub>1"} operates on the original claim while
using @{text "facts\<^sub>1"}. Since the @{command apply} command
@@ -259,12 +261,13 @@
"method\<^sub>3"} will see again a collection of @{text
"facts\<^sub>3"} that has been inserted into the script explicitly.
- \medskip Empirically, any Isar proof method can be categorized as
+ \<^medskip>
+ Empirically, any Isar proof method can be categorized as
follows.
\begin{enumerate}
- \item \emph{Special method with cases} with named context additions
+ \<^enum> \emph{Special method with cases} with named context additions
associated with the follow-up goal state.
Example: @{method "induct"}, which is also a ``raw'' method since it
@@ -272,18 +275,18 @@
Pure conjunction (\secref{sec:logic-aux}), instead of separate
subgoals (\secref{sec:tactical-goals}).
- \item \emph{Structured method} with strong emphasis on facts outside
+ \<^enum> \emph{Structured method} with strong emphasis on facts outside
the goal state.
Example: @{method "rule"}, which captures the key ideas behind
structured reasoning in Isar in its purest form.
- \item \emph{Simple method} with weaker emphasis on facts, which are
+ \<^enum> \emph{Simple method} with weaker emphasis on facts, which are
inserted into subgoals to emulate old-style tactical ``premises''.
Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}.
- \item \emph{Old-style tactic emulation} with detailed numeric goal
+ \<^enum> \emph{Old-style tactic emulation} with detailed numeric goal
addressing and explicit references to entities of the internal goal
state (which are otherwise invisible from proper Isar proof text).
The naming convention @{text "foo_tac"} makes this special
@@ -353,7 +356,8 @@
text %mlex \<open>See also @{command method_setup} in
@{cite "isabelle-isar-ref"} which includes some abstract examples.
- \medskip The following toy examples illustrate how the goal facts
+ \<^medskip>
+ The following toy examples illustrate how the goal facts
and state are passed to proof methods. The predefined proof method
called ``@{method tactic}'' wraps ML source of type @{ML_type
tactic} (abstracted over @{ML_text facts}). This allows immediate
@@ -378,7 +382,9 @@
done
end
-text \<open>\medskip The next example implements a method that simplifies
+text \<open>
+ \<^medskip>
+ The next example implements a method that simplifies
the first subgoal by rewrite rules that are given as arguments.\<close>
method_setup my_simp =
@@ -404,8 +410,8 @@
states are filtered out explicitly to make the raw tactic conform to
standard Isar method behaviour.
- \medskip Method @{method my_simp} can be used in Isar proofs like
- this:
+ \<^medskip>
+ Method @{method my_simp} can be used in Isar proofs like this:
\<close>
notepad
@@ -435,7 +441,9 @@
have "a = c" and "c = b" by (my_simp_all a b)
end
-text \<open>\medskip Apart from explicit arguments, common proof methods
+text \<open>
+ \<^medskip>
+ Apart from explicit arguments, common proof methods
typically work with a default configuration provided by the context. As a
shortcut to rule management we use a cheap solution via the @{command
named_theorems} command to declare a dynamic fact in the context.\<close>
@@ -458,7 +466,8 @@
"rewrite subgoal by given rules and my_simp rules from the context"
text \<open>
- \medskip Method @{method my_simp'} can be used in Isar proofs
+ \<^medskip>
+ Method @{method my_simp'} can be used in Isar proofs
like this:
\<close>
@@ -470,7 +479,9 @@
have "a \<equiv> c" by my_simp'
end
-text \<open>\medskip The @{method my_simp} variants defined above are
+text \<open>
+ \<^medskip>
+ The @{method my_simp} variants defined above are
``simple'' methods, i.e.\ the goal facts are merely inserted as goal
premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper.
For proof methods that are similar to the standard collection of
@@ -485,7 +496,8 @@
"by"}~@{text "my_simp"}'' where @{text "foo"} is not used would
deceive the reader.
- \medskip The technical treatment of rules from the context requires
+ \<^medskip>
+ The technical treatment of rules from the context requires
further attention. Above we rebuild a fresh @{ML_type simpset} from
the arguments and \emph{all} rules retrieved from the context on
every invocation of the method. This does not scale to really large
--- a/src/Doc/Implementation/Logic.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Mon Oct 12 20:58:58 2015 +0200
@@ -36,7 +36,8 @@
The language of types is an uninterpreted order-sorted first-order
algebra; types are qualified by ordered type classes.
- \medskip A \emph{type class} is an abstract syntactic entity
+ \<^medskip>
+ A \emph{type class} is an abstract syntactic entity
declared in the theory context. The \emph{subclass relation} @{text
"c\<^sub>1 \<subseteq> c\<^sub>2"} is specified by stating an acyclic
generating relation; the transitive closure is maintained
@@ -55,7 +56,8 @@
empty one! The intersection of all (finitely many) classes declared
in the current theory is the least element wrt.\ the sort ordering.
- \medskip A \emph{fixed type variable} is a pair of a basic name
+ \<^medskip>
+ A \emph{fixed type variable} is a pair of a basic name
(starting with a @{text "'"} character) and a sort constraint, e.g.\
@{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^sub>s"}.
A \emph{schematic type variable} is a pair of an indexname and a
@@ -96,7 +98,8 @@
completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
(\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
- \medskip The sort algebra is always maintained as \emph{coregular},
+ \<^medskip>
+ The sort algebra is always maintained as \emph{coregular},
which means that type arities are consistent with the subclass
relation: for any type constructor @{text "\<kappa>"}, and classes @{text
"c\<^sub>1 \<subseteq> c\<^sub>2"}, and arities @{text "\<kappa> ::
@@ -242,7 +245,8 @@
corresponding binders. In contrast, free variables and constants
have an explicit name and type in each occurrence.
- \medskip A \emph{bound variable} is a natural number @{text "b"},
+ \<^medskip>
+ A \emph{bound variable} is a natural number @{text "b"},
which accounts for the number of intermediate binders between the
variable occurrence in the body and its binding position. For
example, the de-Bruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would
@@ -263,7 +267,8 @@
e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text
"?x\<^sub>\<tau>"}.
- \medskip A \emph{constant} is a pair of a basic name and a type,
+ \<^medskip>
+ A \emph{constant} is a pair of a basic name and a type,
e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^sub>\<tau>"}
here. Constants are declared in the context as polymorphic families
@{text "c :: \<sigma>"}, meaning that all substitution instances @{text
@@ -287,7 +292,8 @@
polymorphic constants that the user-level type-checker would reject
due to violation of type class restrictions.
- \medskip An \emph{atomic term} is either a variable or constant.
+ \<^medskip>
+ An \emph{atomic term} is either a variable or constant.
The logical category \emph{term} is defined inductively over atomic
terms, with abstraction and application as follows: @{text "t = b |
x\<^sub>\<tau> | ?x\<^sub>\<tau> | c\<^sub>\<tau> | \<lambda>\<^sub>\<tau>. t | t\<^sub>1 t\<^sub>2"}. Parsing and printing takes care of
@@ -320,7 +326,8 @@
name, but different types. In contrast, mixed instances of
polymorphic constants occur routinely.
- \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
+ \<^medskip>
+ The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
is the set of type variables occurring in @{text "t"}, but not in
its type @{text "\<sigma>"}. This means that the term implicitly depends
on type arguments that are not accounted in the result type, i.e.\
@@ -328,14 +335,16 @@
@{text "t\<vartheta>' :: \<sigma>"} with the same type. This slightly
pathological situation notoriously demands additional care.
- \medskip A \emph{term abbreviation} is a syntactic definition @{text
+ \<^medskip>
+ A \emph{term abbreviation} is a syntactic definition @{text
"c\<^sub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
without any hidden polymorphism. A term abbreviation looks like a
constant in the syntax, but is expanded before entering the logical
core. Abbreviations are usually reverted when printing terms, using
@{text "t \<rightarrow> c\<^sub>\<sigma>"} as rules for higher-order rewriting.
- \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
+ \<^medskip>
+ Canonical operations on @{text "\<lambda>"}-terms include @{text
"\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
renaming of bound variables; @{text "\<beta>"}-conversion contracts an
abstraction applied to an argument term, substituting the argument
@@ -569,7 +578,8 @@
the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses
@{text "x : A"} are treated uniformly for propositions and types.}
- \medskip The axiomatization of a theory is implicitly closed by
+ \<^medskip>
+ The axiomatization of a theory is implicitly closed by
forming all instances of type and term variables: @{text "\<turnstile>
A\<vartheta>"} holds for any substitution instance of an axiom
@{text "\<turnstile> A"}. By pushing substitutions through derivations
@@ -602,7 +612,8 @@
correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
the result belongs to a different proof context.
- \medskip An \emph{oracle} is a function that produces axioms on the
+ \<^medskip>
+ An \emph{oracle} is a function that produces axioms on the
fly. Logically, this is an instance of the @{text "axiom"} rule
(\figref{fig:prim-rules}), but there is an operational difference.
The system always records oracle invocations within derivations of
@@ -1036,13 +1047,13 @@
Formulae} in the literature @{cite "Miller:1991"}. Here we give an
inductive characterization as follows:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
@{text "\<^bold>x"} & set of variables \\
@{text "\<^bold>A"} & set of atomic propositions \\
@{text "\<^bold>H = \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
\end{tabular}
- \medskip
+ \<^medskip>
Thus we essentially impose nesting levels on propositions formed
from @{text "\<And>"} and @{text "\<Longrightarrow>"}. At each level there is a prefix
@@ -1054,17 +1065,18 @@
already marks the limit of rule complexity that is usually seen in
practice.
- \medskip Regular user-level inferences in Isabelle/Pure always
+ \<^medskip>
+ 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)"},
+ \<^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
Hereditary Harrop Formula.
- \item The outermost prefix of parameters is represented via
+ \<^item> The outermost prefix of parameters is represented via
schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
\<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
@@ -1225,7 +1237,8 @@
@{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic
polymorphism and type classes are ignored.
- \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
+ \<^medskip>
+ \emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text
"\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text
"p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text
@@ -1233,7 +1246,8 @@
"A"}, and terms @{text "t"} might be suppressed and reconstructed
from the overall proof term.
- \medskip Various atomic proofs indicate special situations within
+ \<^medskip>
+ Various atomic proofs indicate special situations within
the proof construction as follows.
A \emph{bound proof variable} is a natural number @{text "b"} that
@@ -1326,7 +1340,8 @@
using @{text "p \<cdot> TYPE(type)"} (they must appear before any other
term argument of a theorem or axiom, but may be omitted altogether).
- \medskip There are separate read and print operations for proof
+ \<^medskip>
+ There are separate read and print operations for proof
terms, in order to avoid conflicts with the regular term language.
\<close>
@@ -1436,7 +1451,8 @@
recursively explores the graph of the proofs of all theorems being
used here.
- \medskip Alternatively, we may produce a proof term manually, and
+ \<^medskip>
+ Alternatively, we may produce a proof term manually, and
turn it into a theorem as follows:\<close>
ML_val \<open>
@@ -1454,7 +1470,9 @@
|> Drule.export_without_context;
\<close>
-text \<open>\medskip See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}
+text \<open>
+ \<^medskip>
+ See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}
for further examples, with export and import of proof terms via
XML/ML data representation.
\<close>
--- a/src/Doc/Implementation/ML.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/ML.thy Mon Oct 12 20:58:58 2015 +0200
@@ -95,7 +95,8 @@
section headings that are adjacent to plain text, but not other headings
as in the example above.
- \medskip The precise wording of the prose text given in these
+ \<^medskip>
+ The precise wording of the prose text given in these
headings is chosen carefully to introduce the main theme of the
subsequent formal ML text.
\<close>
@@ -111,14 +112,14 @@
variants concerning upper or lower case letters, which are used for
certain ML categories as follows:
- \medskip
+ \<^medskip>
\begin{tabular}{lll}
variant & example & ML categories \\\hline
lower-case & @{ML_text foo_bar} & values, types, record fields \\
capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
\end{tabular}
- \medskip
+ \<^medskip>
For historical reasons, many capitalized names omit underscores,
e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
@@ -188,15 +189,15 @@
\begin{itemize}
- \item A function that maps @{ML_text foo} to @{ML_text bar} is
+ \<^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
bar_for_foo}, nor @{ML_text bar4foo}).
- \item The name component @{ML_text legacy} means that the operation
+ \<^item> The name component @{ML_text legacy} means that the operation
is about to be discontinued soon.
- \item The name component @{ML_text global} means that this works
+ \<^item> The name component @{ML_text global} means that this works
with the background theory instead of the regular local context
(\secref{sec:context}), sometimes for historical reasons, sometimes
due a genuine lack of locality of the concept involved, sometimes as
@@ -205,21 +206,21 @@
application should be migrated to use it with a proper local
context.
- \item Variables of the main context types of the Isabelle/Isar
+ \<^item> Variables of the main context types of the Isabelle/Isar
framework (\secref{sec:context} and \chref{ch:local-theory}) have
firm naming conventions as follows:
\begin{itemize}
- \item theories are called @{ML_text thy}, rarely @{ML_text theory}
+ \<^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
+ \<^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
+ \<^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)
@@ -231,26 +232,26 @@
This allows to emphasize their data flow via plain regular
expressions in the text editor.
- \item The main logical entities (\secref{ch:logic}) have established
+ \<^item> The main logical entities (\secref{ch:logic}) have established
naming convention as follows:
\begin{itemize}
- \item sorts are called @{ML_text S}
-
- \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
+ \<^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
+ \<^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
+ \<^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
+ \<^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> theorems are called @{ML_text th}, or @{ML_text thm}
\end{itemize}
@@ -379,7 +380,8 @@
to changes of the initial text (working against
\emph{maintainability}) etc.
- \medskip For similar reasons, any kind of two-dimensional or tabular
+ \<^medskip>
+ For similar reasons, any kind of two-dimensional or tabular
layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
avoided.
@@ -447,12 +449,13 @@
but help to analyse the nesting based on character matching in the
text editor.
- \medskip There are two main exceptions to the overall principle of
+ \<^medskip>
+ There are two main exceptions to the overall principle of
compositionality in the layout of complex expressions.
\begin{enumerate}
- \item @{ML_text "if"} expressions are iterated as if ML had multi-branch
+ \<^enum> @{ML_text "if"} expressions are iterated as if ML had multi-branch
conditionals, e.g.
\begin{verbatim}
@@ -463,7 +466,7 @@
else e3
\end{verbatim}
- \item @{ML_text fn} abstractions are often layed-out as if they
+ \<^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:
@@ -515,7 +518,8 @@
... end
\end{verbatim}
- \medskip In general the source layout is meant to emphasize the
+ \<^medskip>
+ In general the source layout is meant to emphasize the
structure of complex language expressions, not to pretend that SML
had a completely different syntax (say that of Haskell, Scala, Java).
\<close>
@@ -584,10 +588,11 @@
compilation within independent nodes of the implicit theory development
graph.}
- \medskip The next example shows how to embed ML into Isar proofs, using
+ \<^medskip>
+ The next example shows how to embed ML into Isar proofs, using
@{command_ref "ML_prf"} instead of @{command_ref "ML"}. As illustrated
below, the effect on the ML environment is local to the whole proof body,
- but ignoring the block structure. \<close>
+ but ignoring the block structure.\<close>
notepad
begin
@@ -603,7 +608,8 @@
manipulate corresponding entities, e.g.\ export a fact from a block
context.
- \medskip Two further ML commands are useful in certain situations:
+ \<^medskip>
+ Two further ML commands are useful in certain situations:
@{command_ref ML_val} and @{command_ref ML_command} are \emph{diagnostic} in
the sense that there is no effect on the underlying environment, and can
thus be used anywhere. The examples below produce long strings of digits by
@@ -681,7 +687,8 @@
Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
defined in @{cite "isabelle-isar-ref"}.
- \medskip A regular antiquotation @{text "@{name args}"} processes
+ \<^medskip>
+ A regular antiquotation @{text "@{name args}"} processes
its arguments by the usual means of the Isar source language, and
produces corresponding ML source text, either as literal
\emph{inline} text (e.g.\ @{text "@{term t}"}) or abstract
@@ -781,7 +788,8 @@
\<alpha>"} or @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"} (the latter is not
present in the Isabelle/ML library).
- \medskip The main idea is that arguments that vary less are moved
+ \<^medskip>
+ The main idea is that arguments that vary less are moved
further to the left than those that vary more. Two particularly
important categories of functions are \emph{selectors} and
\emph{updates}.
@@ -830,27 +838,28 @@
improved by introducing \emph{forward} versions of application and
composition as follows:
- \medskip
+ \<^medskip>
\begin{tabular}{lll}
@{text "x |> f"} & @{text "\<equiv>"} & @{text "f x"} \\
@{text "(f #> g) x"} & @{text "\<equiv>"} & @{text "x |> f |> g"} \\
\end{tabular}
- \medskip
+ \<^medskip>
This enables to write conveniently @{text "x |> f\<^sub>1 |> \<dots> |> f\<^sub>n"} or
@{text "f\<^sub>1 #> \<dots> #> f\<^sub>n"} for its functional abstraction over @{text
"x"}.
- \medskip There is an additional set of combinators to accommodate
+ \<^medskip>
+ There is an additional set of combinators to accommodate
multiple results (via pairs) that are passed on as multiple
arguments (via currying).
- \medskip
+ \<^medskip>
\begin{tabular}{lll}
@{text "(x, y) |-> f"} & @{text "\<equiv>"} & @{text "f x y"} \\
@{text "(f #-> g) x"} & @{text "\<equiv>"} & @{text "x |> f |-> g"} \\
\end{tabular}
- \medskip
+ \<^medskip>
\<close>
text %mlref \<open>
@@ -944,7 +953,8 @@
memory (``deforestation''), but it requires some practice to read
and write fluently.
- \medskip The next example elaborates the idea of canonical
+ \<^medskip>
+ The next example elaborates the idea of canonical
iteration, demonstrating fast accumulation of tree content using a
text buffer.
\<close>
@@ -1094,7 +1104,8 @@
\<close>
text \<open>
- \medskip An alternative is to make a paragraph of freely-floating words as
+ \<^medskip>
+ An alternative is to make a paragraph of freely-floating words as
follows.
\<close>
@@ -1154,7 +1165,8 @@
ML runtime system attaches detailed source position stemming from the
corresponding @{ML_text raise} keyword.
- \medskip User modules can always introduce their own custom
+ \<^medskip>
+ User modules can always introduce their own custom
exceptions locally, e.g.\ to organize internal failures robustly
without overlapping with existing exceptions. Exceptions that are
exposed in module signatures require extra care, though, and should
@@ -1266,23 +1278,23 @@
\begin{enumerate}
- \item a single ASCII character ``@{text "c"}'', for example
+ \<^enum> a single ASCII character ``@{text "c"}'', for example
``@{verbatim a}'',
- \item a codepoint according to UTF-8 (non-ASCII byte sequence),
-
- \item a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}@{text
+ \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
+
+ \<^enum> a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}@{text
"ident"}@{verbatim ">"}'', for example ``@{verbatim "\<alpha>"}'',
- \item a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}@{text
+ \<^enum> a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}@{text
"ident"}@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'',
- \item a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}@{text
+ \<^enum> a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}@{text
text}@{verbatim ">"}'' where @{text text} consists of printable characters
excluding ``@{verbatim "."}'' and ``@{verbatim ">"}'', for example
``@{verbatim "\<^raw:$\sum_{i = 1}^n$>"}'',
- \item a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
+ \<^enum> a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
"<^raw"}@{text n}@{verbatim ">"}, where @{text n} consists of digits, for
example ``@{verbatim "\<^raw42>"}''.
@@ -1303,7 +1315,8 @@
mathematical symbols, but within the core Isabelle/ML world there is no link
to the standard collection of Isabelle regular symbols.
- \medskip Output of Isabelle symbols depends on the print mode. For example,
+ \<^medskip>
+ Output of Isabelle symbols depends on the print mode. For example,
the standard {\LaTeX} setup of the Isabelle document preparation system
would present ``@{verbatim "\<alpha>"}'' as @{text "\<alpha>"}, and ``@{verbatim
"\<^bold>\<alpha>"}'' as @{text "\<^bold>\<alpha>"}. On-screen rendering usually works by mapping a
@@ -1415,10 +1428,10 @@
\begin{enumerate}
- \item sequence of Isabelle symbols (see also \secref{sec:symbols}),
+ \<^enum> 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"}),
+ \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}),
with @{ML YXML.parse_body} as key operation.
\end{enumerate}
@@ -1710,7 +1723,8 @@
speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be expected
@{cite "Wenzel:2013:ITP"}.
- \medskip ML threads lack the memory protection of separate
+ \<^medskip>
+ ML threads lack the memory protection of separate
processes, and operate concurrently on shared heap memory. This has
the advantage that results of independent computations are directly
available to other threads: abstract values can be passed without
@@ -1750,15 +1764,15 @@
\begin{itemize}
- \item Global references (or arrays), i.e.\ mutable memory cells that
+ \<^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
mutable values in the toplevel scope.}
- \item Global state of the running Isabelle/ML process, i.e.\ raw I/O
+ \<^item> Global state of the running Isabelle/ML process, i.e.\ raw I/O
channels, environment variables, current working directory.
- \item Writable resources in the file-system that are shared among
+ \<^item> Writable resources in the file-system that are shared among
different threads or external processes.
\end{itemize}
@@ -1771,7 +1785,7 @@
\begin{itemize}
- \item Avoid global references altogether. Isabelle/Isar maintains a
+ \<^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
plain value and user tools can get/map their own data in a purely
@@ -1779,7 +1793,7 @@
(\secref{sec:config-options}) provide simple drop-in replacements
for historic reference variables.
- \item Keep components with local state information re-entrant.
+ \<^item> Keep components with local state information re-entrant.
Instead of poking initial values into (private) global references, a
new state record can be created on each invocation, and passed
through any auxiliary functions of the component. The state record
@@ -1787,7 +1801,7 @@
synchronization, as long as each invocation gets its own copy and the
tool itself is single-threaded.
- \item Avoid raw output on @{text "stdout"} or @{text "stderr"}. The
+ \<^item> Avoid raw output on @{text "stdout"} or @{text "stderr"}. The
Poly/ML library is thread-safe for each individual output operation,
but the ordering of parallel invocations is arbitrary. This means
raw output will appear on some system console with unpredictable
@@ -1801,10 +1815,10 @@
only happen when commands use parallelism internally (and only at
message boundaries).
- \item Treat environment variables and the current working directory
+ \<^item> Treat environment variables and the current working directory
of the running process as read-only.
- \item Restrict writing to the file-system to unique temporary files.
+ \<^item> Restrict writing to the file-system to unique temporary files.
Isabelle already provides a temporary directory that is unique for
the running process, and there is a centralized source of unique
serial numbers in Isabelle/ML. Thus temporary files that are passed
@@ -1913,7 +1927,9 @@
@{assert} (a <> b);
\<close>
-text \<open>\medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
+text \<open>
+ \<^medskip>
+ See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
to implement a mailbox as synchronized variable over a purely
functional list.\<close>
@@ -1933,7 +1949,8 @@
evaluation via futures, asynchronous evaluation via promises,
evaluation with time limit etc.
- \medskip An \emph{unevaluated expression} is represented either as
+ \<^medskip>
+ An \emph{unevaluated expression} is represented either as
unit abstraction @{verbatim "fn () => a"} of type
@{verbatim "unit -> 'a"} or as regular function
@{verbatim "fn a => b"} of type @{verbatim "'a -> 'b"}. Both forms
@@ -1948,7 +1965,8 @@
be cascaded to modify a given function, before it is ultimately
applied to some argument.
- \medskip \emph{Reified results} make the disjoint sum of regular
+ \<^medskip>
+ \emph{Reified results} make the disjoint sum of regular
values versions exceptional situations explicit as ML datatype:
@{text "'a result = Res of 'a | Exn of exn"}. This is typically
used for administrative purposes, to store the overall outcome of an
@@ -2158,7 +2176,8 @@
threads that get activated in certain explicit wait conditions, after a
timeout.
- \medskip Each future task belongs to some \emph{task group}, which
+ \<^medskip>
+ Each future task belongs to some \emph{task group}, which
represents the hierarchic structure of related tasks, together with the
exception status a that point. By default, the task group of a newly created
future is a new sub-group of the presently running one, but it is also
@@ -2173,7 +2192,8 @@
tasks that lack regular result information, will pick up parallel exceptions
from the cumulative group status.
- \medskip A \emph{passive future} or \emph{promise} is a future with slightly
+ \<^medskip>
+ A \emph{passive future} or \emph{promise} is a future with slightly
different evaluation policies: there is only a single-assignment variable
and some expression to evaluate for the \emph{failed} case (e.g.\ to clean
up resources when canceled). A regular result is produced by external means,
@@ -2217,19 +2237,19 @@
\begin{itemize}
- \item @{text "name : string"} (default @{ML "\"\""}) specifies a common name
+ \<^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
+ \<^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
+ \<^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
+ \<^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}.
@@ -2242,7 +2262,7 @@
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
+ \<^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.
--- a/src/Doc/Implementation/Prelim.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Mon Oct 12 20:58:58 2015 +0200
@@ -22,17 +22,18 @@
@{text "\<Gamma> \<turnstile> \<phi>"} is strictly limited to Simple Type Theory (with
fixed type variables in the assumptions).
- \medskip Contexts and derivations are linked by the following key
+ \<^medskip>
+ Contexts and derivations are linked by the following key
principles:
\begin{itemize}
- \item Transfer: monotonicity of derivations admits results to be
+ \<^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>'
\<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
- \item Export: discharge of hypotheses admits results to be exported
+ \<^item> Export: discharge of hypotheses admits results to be exported
into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}
implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and
@{text "\<Delta> = \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here,
@@ -40,7 +41,8 @@
\end{itemize}
- \medskip By modeling the main characteristics of the primitive
+ \<^medskip>
+ By modeling the main characteristics of the primitive
@{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any
particular logical content, we arrive at the fundamental notions of
\emph{theory context} and \emph{proof context} in Isabelle/Isar.
@@ -60,7 +62,8 @@
standard proof steps implicitly (cf.\ the @{text "rule"} method
@{cite "isabelle-isar-ref"}).
- \medskip Thus Isabelle/Isar is able to bring forth more and more
+ \<^medskip>
+ Thus Isabelle/Isar is able to bring forth more and more
concepts successively. In particular, an object-logic like
Isabelle/HOL continues the Isabelle/Pure setup by adding specific
components for automated reasoning (classical reasoner, tableau
@@ -85,7 +88,8 @@
nameless incremental updates, until the final @{text "end"} operation is
performed.
- \medskip The example in \figref{fig:ex-theory} below shows a theory
+ \<^medskip>
+ The example in \figref{fig:ex-theory} below shows a theory
graph derived from @{text "Pure"}, with theory @{text "Length"}
importing @{text "Nat"} and @{text "List"}. The body of @{text
"Length"} consists of a sequence of updates, resulting in locally a
@@ -109,7 +113,8 @@
\end{center}
\end{figure}
- \medskip Derived formal entities may retain a reference to the
+ \<^medskip>
+ Derived formal entities may retain a reference to the
background theory in order to indicate the formal context from which
they were produced. This provides an immutable certificate of the
background theory.\<close>
@@ -303,14 +308,14 @@
\paragraph{Theory data} declarations need to implement the following
ML signature:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
@{text "\<type> T"} & representing type \\
@{text "\<val> empty: T"} & empty default value \\
@{text "\<val> extend: T \<rightarrow> T"} & re-initialize on import \\
@{text "\<val> merge: T \<times> T \<rightarrow> T"} & join on import \\
\end{tabular}
- \medskip
+ \<^medskip>
The @{text "empty"} value acts as initial default for \emph{any}
theory that does not declare actual data content; @{text "extend"}
@@ -329,12 +334,12 @@
\paragraph{Proof context data} declarations need to implement the
following ML signature:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
@{text "\<type> T"} & representing type \\
@{text "\<val> init: theory \<rightarrow> T"} & produce initial value \\
\end{tabular}
- \medskip
+ \<^medskip>
The @{text "init"} operation is supposed to produce a pure value
from the given background theory and should be somehow
@@ -352,16 +357,17 @@
predefined to select the current data value from the background
theory.
- \bigskip Any of the above data declarations over type @{text "T"}
+ \<^bigskip>
+ Any of the above data declarations over type @{text "T"}
result in an ML structure with the following signature:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
@{text "get: context \<rightarrow> T"} \\
@{text "put: T \<rightarrow> context \<rightarrow> context"} \\
@{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context"} \\
\end{tabular}
- \medskip
+ \<^medskip>
These other operations provide exclusive access for the particular
kind of context (theory, proof, or generic context). This interface
@@ -448,13 +454,14 @@
exponential blowup. Plain list append etc.\ must never be used for
theory data merges!
- \medskip Our intended invariant is achieved as follows:
+ \<^medskip>
+ Our intended invariant is achieved as follows:
\begin{enumerate}
- \item @{ML Wellformed_Terms.add} only admits terms that have passed
+ \<^enum> @{ML Wellformed_Terms.add} only admits terms that have passed
the @{ML Sign.cert_term} check of the given theory at that point.
- \item Wellformedness in the sense of @{ML Sign.cert_term} is
+ \<^enum> Wellformedness in the sense of @{ML Sign.cert_term} is
monotonic wrt.\ the sub-theory relation. So our data can move
upwards in the hierarchy (via extension or merges), and maintain
wellformedness without further checks.
@@ -610,17 +617,18 @@
e.g.\ the string ``@{verbatim \<alpha>}'' encodes as a single
symbol (\secref{sec:symbols}).
- \medskip Subsequently, we shall introduce specific categories of
+ \<^medskip>
+ 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
+ \<^item> Basic names (\secref{sec:basic-name}): free and bound
variables.
- \item Indexed names (\secref{sec:indexname}): schematic variables.
+ \<^item> Indexed names (\secref{sec:indexname}): schematic variables.
- \item Long names (\secref{sec:long-name}): constants of any kind
+ \<^item> Long names (\secref{sec:long-name}): constants of any kind
(type constructors, term constants, other concepts defined in user
space). Such entities are typically managed via name spaces
(\secref{sec:name-space}).
@@ -648,7 +656,8 @@
as internal, which prevents mysterious names like @{text "xaa"} to
appear in human-readable text.
- \medskip Manipulating binding scopes often requires on-the-fly
+ \<^medskip>
+ Manipulating binding scopes often requires on-the-fly
renamings. A \emph{name context} contains a collection of already
used names. The @{text "declare"} operation adds names to the
context.
@@ -725,8 +734,9 @@
@{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
\<close>
-text \<open>\medskip The same works relatively to the formal context as
- follows.\<close>
+text \<open>
+ \<^medskip>
+ The same works relatively to the formal context as follows.\<close>
experiment fixes a b c :: 'a
begin
@@ -761,16 +771,17 @@
indexed names: then @{text "(x, -1)"} is used to encode the basic
name @{text "x"}.
- \medskip Isabelle syntax observes the following rules for
+ \<^medskip>
+ 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 "?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 "?xi"} if @{text "x"} does not end with a digit,
- \item @{text "?x.i"} otherwise.
+ \<^item> @{text "?x.i"} otherwise.
\end{itemize}
@@ -861,13 +872,15 @@
"declare"} operation augments a name space according to the accesses
determined by a given binding, and a naming policy from the context.
- \medskip A @{text "binding"} specifies details about the prospective
+ \<^medskip>
+ A @{text "binding"} specifies details about the prospective
long name of a newly introduced formal entity. It consists of a
base name, prefixes for qualification (separate ones for system
infrastructure and user-space mechanisms), a slot for the original
source position, and some additional flags.
- \medskip A @{text "naming"} provides some additional details for
+ \<^medskip>
+ A @{text "naming"} provides some additional details for
producing a long name from a binding. Normally, the naming is
implicit in the theory or proof context. The @{text "full"}
operation (and its variants for different context types) produces a
@@ -875,12 +888,13 @@
main equation of this ``chemical reaction'' when binding new
entities in a context is as follows:
- \medskip
+ \<^medskip>
\begin{tabular}{l}
@{text "binding + naming \<longrightarrow> long name + name space accesses"}
\end{tabular}
- \bigskip As a general principle, there is a separate name space for
+ \<^bigskip>
+ As a general principle, there is a separate name space for
each kind of formal entity, e.g.\ fact, logical constant, type
constructor, type class. It is usually clear from the occurrence in
concrete syntax (or from the scope) which kind of entity a name
@@ -897,7 +911,7 @@
qualification. This leads to the following conventions for derived
names:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
logical entity & fact name \\\hline
constant @{text "c"} & @{text "c.intro"} \\
@@ -1041,8 +1055,9 @@
ML_val \<open>Binding.pos_of @{binding here}\<close>
-text \<open>\medskip That position can be also printed in a message as
- follows:\<close>
+text \<open>
+ \<^medskip>
+ That position can be also printed in a message as follows:\<close>
ML_command
\<open>writeln
@@ -1053,7 +1068,8 @@
additional information for feedback given to the user (error
messages etc.).
- \medskip The following example refers to its source position
+ \<^medskip>
+ The following example refers to its source position
directly, which is occasionally useful for experimentation and
diagnostic purposes:\<close>
--- a/src/Doc/Implementation/Proof.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Proof.thy Mon Oct 12 20:58:58 2015 +0200
@@ -30,7 +30,8 @@
@{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile> \<forall>\<alpha>. B(\<alpha>)"}''
without demanding a truly polymorphic framework.
- \medskip Additional care is required to treat type variables in a
+ \<^medskip>
+ Additional care is required to treat type variables in a
way that facilitates type-inference. In principle, term variables
depend on type variables, which means that type variables would have
to be declared first. For example, a raw type-theoretic framework
@@ -237,7 +238,8 @@
A\<^sub>n \<turnstile> B"} where @{text "A\<^sub>1, \<dots>, A\<^sub>n"} needs to
be covered by the assumptions of the current context.
- \medskip The @{text "add_assms"} operation augments the context by
+ \<^medskip>
+ The @{text "add_assms"} operation augments the context by
local assumptions, which are parameterized by an arbitrary @{text
"export"} rule (see below).
@@ -249,7 +251,8 @@
separate flag to indicate a goal context, where the result is meant
to refine an enclosing sub-goal of a structured proof state.
- \medskip The most basic export rule discharges assumptions directly
+ \<^medskip>
+ The most basic export rule discharges assumptions directly
by means of the @{text "\<Longrightarrow>"} introduction rule:
\[
\infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
@@ -262,7 +265,8 @@
\infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
\]
- \medskip Alternative versions of assumptions may perform arbitrary
+ \<^medskip>
+ Alternative versions of assumptions may perform arbitrary
transformations on export, as long as the corresponding portion of
hypotheses is removed from the given facts. For example, a local
definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
@@ -354,7 +358,8 @@
references to free variables or assumptions not present in the proof
context.
- \medskip The @{text "SUBPROOF"} combinator allows to structure a
+ \<^medskip>
+ The @{text "SUBPROOF"} combinator allows to structure a
tactical proof recursively by decomposing a selected sub-goal:
@{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
after fixing @{text "x"} and assuming @{text "A(x)"}. This means
@@ -482,7 +487,9 @@
sorry
end
-text \<open>\medskip The next example demonstrates forward-elimination in
+text \<open>
+ \<^medskip>
+ The next example demonstrates forward-elimination in
a local context, using @{ML Obtain.result}.\<close>
notepad
--- a/src/Doc/Implementation/Syntax.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Syntax.thy Mon Oct 12 20:58:58 2015 +0200
@@ -25,7 +25,8 @@
users. Beginners often stumble over unexpectedly general types inferred by
the system.}
- \medskip The main inner syntax operations are \emph{read} for
+ \<^medskip>
+ The main inner syntax operations are \emph{read} for
parsing together with type-checking, and \emph{pretty} for formatted
output. See also \secref{sec:read-print}.
@@ -37,9 +38,9 @@
\begin{itemize}
- \item @{text "read = parse; check"}
+ \<^item> @{text "read = parse; check"}
- \item @{text "pretty = uncheck; unparse"}
+ \<^item> @{text "pretty = uncheck; unparse"}
\end{itemize}
@@ -49,7 +50,8 @@
"check"}. Note that the formal status of bound variables, versus free
variables, versus constants must not be changed between these phases.
- \medskip In general, @{text check} and @{text uncheck} operate
+ \<^medskip>
+ In general, @{text check} and @{text uncheck} operate
simultaneously on a list of terms. This is particular important for
type-checking, to reconstruct types for several terms of the same context
and scope. In contrast, @{text parse} and @{text unparse} operate separately
@@ -131,7 +133,8 @@
@{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML
Syntax.string_of_term} are the most important operations in practice.
- \medskip Note that the string values that are passed in and out are
+ \<^medskip>
+ Note that the string values that are passed in and out are
annotated by the system, to carry further markup that is relevant for the
Prover IDE @{cite "isabelle-jedit"}. User code should neither compose its
own input strings, nor try to analyze the output strings. Conceptually this
@@ -223,7 +226,8 @@
contracted during the @{text "uncheck"} phase, without affecting the
type-assignment of the given terms.
- \medskip The precise meaning of type checking depends on the context ---
+ \<^medskip>
+ The precise meaning of type checking depends on the context ---
additional check/uncheck modules might be defined in user space.
For example, the @{command class} command defines a context where
--- a/src/Doc/Implementation/Tactic.thy Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy Mon Oct 12 20:58:58 2015 +0200
@@ -41,7 +41,8 @@
"#C"} here. This ensures that the decomposition into subgoals and
main conclusion is well-defined for arbitrarily structured claims.
- \medskip Basic goal management is performed via the following
+ \<^medskip>
+ Basic goal management is performed via the following
Isabelle/Pure rules:
\[
@@ -49,7 +50,8 @@
\infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
\]
- \medskip The following low-level variants admit general reasoning
+ \<^medskip>
+ The following low-level variants admit general reasoning
with protected propositions:
\[
@@ -115,7 +117,8 @@
combinators for building proof tools that involve search
systematically, see also \secref{sec:tacticals}.
- \medskip As explained before, a goal state essentially consists of a
+ \<^medskip>
+ As explained before, a goal state essentially consists of a
list of subgoals that imply the main goal (conclusion). Tactics may
operate on all subgoals or on a particularly specified subgoal, but
must not change the main conclusion (apart from instantiating
@@ -143,22 +146,23 @@
index as @{text "int"} argument in full generality; a hardwired
subgoal 1 is not acceptable.
- \medskip The main well-formedness conditions for proper tactics are
+ \<^medskip>
+ 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
+ \<^item> General tactic failure is indicated by an empty result, only
serious faults may produce an exception.
- \item The main conclusion must not be changed, apart from
+ \<^item> The main conclusion must not be changed, apart from
instantiating schematic variables.
- \item A tactic operates either uniformly on all subgoals, or
+ \<^item> A tactic operates either uniformly on all subgoals, or
specifically on a selected subgoal (without bumping into unrelated
subgoals).
- \item Range errors in subgoal addressing produce an empty result.
+ \<^item> Range errors in subgoal addressing produce an empty result.
\end{itemize}
@@ -251,7 +255,8 @@
Assumption tactics close a subgoal by unifying some of its premises
against its conclusion.
- \medskip All the tactics in this section operate on a subgoal
+ \<^medskip>
+ All the tactics in this section operate on a subgoal
designated by a positive integer. Other subgoals might be affected
indirectly, due to instantiation of schematic variables.
@@ -261,12 +266,12 @@
\begin{enumerate}
- \item selecting one of the rules given as argument to the tactic;
+ \<^enum> selecting one of the rules given as argument to the tactic;
- \item selecting a subgoal premise to eliminate, unifying it against
+ \<^enum> selecting a subgoal premise to eliminate, unifying it against
the first premise of the rule;
- \item unifying the conclusion of the subgoal to the conclusion of
+ \<^enum> unifying the conclusion of the subgoal to the conclusion of
the rule.
\end{enumerate}
@@ -366,7 +371,8 @@
"?P"}, according to the shape of the given subgoal. This is
sufficiently well-behaved in most practical situations.
- \medskip Isabelle provides separate versions of the standard @{text
+ \<^medskip>
+ Isabelle provides separate versions of the standard @{text
"r/e/d/f"} resolution tactics that allow to provide explicit
instantiations of unknowns of the given rule, wrt.\ terms that refer
to the implicit context of the selected subgoal.
@@ -675,15 +681,15 @@
\begin{itemize}
- \item @{ML all_tac} is the identity element of the tactical @{ML_op
+ \<^item> @{ML all_tac} is the identity element of the tactical @{ML_op
"THEN"}.
- \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
+ \<^item> @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
@{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"},
which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is
equivalent to @{ML no_tac}.
- \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
+ \<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
functions over more basic combinators (ignoring some internal
implementation tricks):