# 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 :: \"} assigns a (unique) type to a term according to the structure of atomic terms, abstractions, and - applicatins: + applications: \[ \infer{@{text "a\<^sub>\ :: \"}}{} \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,,'', 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::\"} are fixed *} { - have "x::'a \ x" -- {* implicit type assigment by concrete occurrence *} + have "x::'a \ 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}