--- a/src/Doc/Implementation/Isar.thy Mon Apr 14 23:26:52 2014 +0200
+++ b/src/Doc/Implementation/Isar.thy Tue Apr 15 00:03:39 2014 +0200
@@ -115,7 +115,7 @@
\item @{ML Proof.raw_goal}~@{text "state"} returns the structured
Isar goal (if available) in the raw internal form seen by ``raw''
methods (like @{method induct}). This form is rarely appropriate
- for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
+ for diagnostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
should be used in most situations.
\item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"}
@@ -355,7 +355,7 @@
\cite{isabelle-isar-ref} which includes some abstract examples.
\medskip The following toy examples illustrate how the goal facts
- and state are passed to proof methods. The pre-defined proof method
+ 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
experimentation without parsing of concrete syntax. *}
--- a/src/Doc/Implementation/Logic.thy Mon Apr 14 23:26:52 2014 +0200
+++ b/src/Doc/Implementation/Logic.thy Tue Apr 15 00:03:39 2014 +0200
@@ -297,7 +297,7 @@
The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
term according to the structure of atomic terms, abstractions, and
- applicatins:
+ applications:
\[
\infer{@{text "a\<^sub>\<tau> :: \<tau>"}}{}
\qquad
--- a/src/Doc/Implementation/ML.thy Mon Apr 14 23:26:52 2014 +0200
+++ b/src/Doc/Implementation/ML.thy Tue Apr 15 00:03:39 2014 +0200
@@ -229,7 +229,7 @@
\end{itemize}
Variations with primed or decimal numbers are always possible, as
- well as sematic prefixes like @{ML_text foo_thy} or @{ML_text
+ well as semantic prefixes like @{ML_text foo_thy} or @{ML_text
bar_ctxt}, but the base conventions above need to be preserved.
This allows to visualize the their data flow via plain regular
expressions in the editor.
@@ -764,7 +764,7 @@
etc. How well this works in practice depends on the order of
arguments. In the worst case, arguments are arranged erratically,
and using a function in a certain situation always requires some
- glue code. Thus we would get exponentially many oppurtunities to
+ glue code. Thus we would get exponentially many opportunities to
decorate the code with meaningless permutations of arguments.
This can be avoided by \emph{canonical argument order}, which
@@ -1148,7 +1148,7 @@
producing a console interrupt manually etc. An Isabelle/ML program
that intercepts interrupts becomes dependent on physical effects of
the environment. Even worse, exception handling patterns that are
- too general by accident, e.g.\ by mispelled exception constructors,
+ too general by accident, e.g.\ by misspelled exception constructors,
will cover interrupts unintentionally and thus render the program
semantics ill-defined.
@@ -1246,7 +1246,7 @@
\item a single ASCII character ``@{text "c"}'', for example
``\verb,a,'',
- \item a codepoint according to UTF8 (non-ASCII byte sequence),
+ \item a codepoint according to UTF-8 (non-ASCII byte sequence),
\item a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
--- a/src/Doc/Implementation/Proof.thy Mon Apr 14 23:26:52 2014 +0200
+++ b/src/Doc/Implementation/Proof.thy Tue Apr 15 00:03:39 2014 +0200
@@ -63,7 +63,7 @@
{
fix x -- {* all potential occurrences of some @{text "x::\<tau>"} are fixed *}
{
- have "x::'a \<equiv> x" -- {* implicit type assigment by concrete occurrence *}
+ have "x::'a \<equiv> x" -- {* implicit type assignment by concrete occurrence *}
by (rule reflexive)
}
thm this -- {* result still with fixed type @{text "'a"} *}
@@ -75,7 +75,7 @@
vs.\ type variables, with high-level principles for moving the
frontier between fixed and schematic variables.
- The @{text "add_fixes"} operation explictly declares fixed
+ The @{text "add_fixes"} operation explicitly declares fixed
variables; the @{text "declare_term"} operation absorbs a term into
a context by fixing new type variables and adding syntactic
constraints.
@@ -198,7 +198,7 @@
@{text x1}, @{text x2}, @{text x3}, without depending on
the details on the system policy for introducing these variants.
Recall that within a proof body the system always invents fresh
- ``skolem constants'', e.g.\ as follows: *}
+ ``Skolem constants'', e.g.\ as follows: *}
notepad
begin
@@ -437,7 +437,7 @@
it. The latter may depend on the local assumptions being presented
as facts. The result is in HHF normal form.
- \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
+ \item @{ML Goal.prove_multi} is similar to @{ML Goal.prove}, but
states several conclusions simultaneously. The goal is encoded by
means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
into a collection of individual subgoals.
--- a/src/Doc/Implementation/Tactic.thy Mon Apr 14 23:26:52 2014 +0200
+++ b/src/Doc/Implementation/Tactic.thy Tue Apr 15 00:03:39 2014 +0200
@@ -431,7 +431,7 @@
\item @{ML rename_tac}~@{text "names i"} renames the innermost
parameters of subgoal @{text i} according to the provided @{text
- names} (which need to be distinct indentifiers).
+ names} (which need to be distinct identifiers).
\end{description}