# HG changeset patch
# User wenzelm
# Date 1397513019 -7200
# Node ID 4c94f631c5951faff758ecf2df582e3f82b75957
# Parent  e73723b39c829354c7bb353582318a968a810181
tuned spelling;

diff -r e73723b39c82 -r 4c94f631c595 src/Doc/Implementation/Isar.thy
--- 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. *}
diff -r e73723b39c82 -r 4c94f631c595 src/Doc/Implementation/Logic.thy
--- 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
diff -r e73723b39c82 -r 4c94f631c595 src/Doc/Implementation/ML.thy
--- 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>,'',
diff -r e73723b39c82 -r 4c94f631c595 src/Doc/Implementation/Proof.thy
--- 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.
diff -r e73723b39c82 -r 4c94f631c595 src/Doc/Implementation/Tactic.thy
--- 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}