--- 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: