# 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 "\"}, 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}