# HG changeset patch
# User wenzelm
# Date 1397514091 -7200
# Node ID f05b7d6ec5924e454f469ff627ec41ee5fe39c8d
# Parent  af3e6576e680fc83392f08a5dd5cfc14291a50a9
tuned spelling;

diff -r af3e6576e680 -r f05b7d6ec592 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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.
diff -r af3e6576e680 -r f05b7d6ec592 src/Doc/Isar_Ref/Misc.thy
--- 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.
 
diff -r af3e6576e680 -r f05b7d6ec592 src/Doc/Isar_Ref/Proof.thy
--- 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}