# HG changeset patch
# User nipkow
# Date 1394728616 -3600
# Node ID bdc03e91684a9681f8a0f52d8f0bd0ab2404ac5c
# Parent  9bf84c452463009d3889d3348e11fd18ddbfccae
typos

diff -r 9bf84c452463 -r bdc03e91684a src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Thu Mar 13 16:39:08 2014 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Thu Mar 13 17:36:56 2014 +0100
@@ -811,7 +811,7 @@
 step': "star' r x y \<Longrightarrow> r y z \<Longrightarrow> star' r x z"
 
 text{*
-The single @{text r} step is performer after rather than before the @{text star'}
+The single @{text r} step is performed after rather than before the @{text star'}
 steps. Prove @{prop "star' r x y \<Longrightarrow> star r x y"} and
 @{prop "star r x y \<Longrightarrow> star r' x y"}. You may need lemmas.
 Note that rule induction fails
@@ -829,7 +829,7 @@
 \begin{exercise}
 A context-free grammar can be seen as an inductive definition where each
 nonterminal $A$ is an inductively defined predicate on lists of terminal
-symbols: $A(w)$ mans that $w$ is in the language generated by $A$.
+symbols: $A(w)$ means that $w$ is in the language generated by $A$.
 For example, the production $S \to a S b$ can be viewed as the implication
 @{prop"S w \<Longrightarrow> S (a # w @ [b])"} where @{text a} and @{text b} are terminal symbols,
 i.e., elements of some alphabet. The alphabet can be defined like this: