--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Apr 15 00:14:57 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Apr 15 00:21:31 2014 +0200
@@ -1119,7 +1119,7 @@
subsubsection {* AST constants versus variables *}
text {* Depending on the situation --- input syntax, output syntax,
- translation patterns --- the distinction of atomic asts as @{ML
+ translation patterns --- the distinction of atomic ASTs as @{ML
Ast.Constant} versus @{ML Ast.Variable} serves slightly different
purposes.
@@ -1266,7 +1266,7 @@
\end{itemize}
Each @{text "A\<^sub>i"} is decorated by priority @{text "p\<^sub>i"} from the
- given list @{text "ps"}; misssing priorities default to 0.
+ given list @{text "ps"}; missing priorities default to 0.
The resulting nonterminal of the production is determined similarly
from type @{text "\<tau>"}, with priority @{text "q"} and default 1000.
--- a/src/Doc/Isar_Ref/Misc.thy Tue Apr 15 00:14:57 2014 +0200
+++ b/src/Doc/Isar_Ref/Misc.thy Tue Apr 15 00:21:31 2014 +0200
@@ -133,7 +133,7 @@
\item @{command "pwd"} prints the current working directory.
- \item @{command "use_thy"}~@{text A} preload theory @{text A}.
+ \item @{command "use_thy"}~@{text A} preloads theory @{text A}.
These system commands are scarcely used when working interactively,
since loading of theories is done automatically as required.
--- a/src/Doc/Isar_Ref/Proof.thy Tue Apr 15 00:14:57 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Apr 15 00:21:31 2014 +0200
@@ -495,7 +495,7 @@
resulting error as a warning beforehand. Watch out for the
following message:
- %FIXME proper antiquitation
+ %FIXME proper antiquotation
\begin{ttbox}
Problem! Local statement will fail to solve any pending goal
\end{ttbox}