--- a/src/Doc/Prog_Prove/Logic.thy Tue Aug 08 23:55:33 2023 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Wed Aug 09 08:24:24 2023 +0200
@@ -841,7 +841,7 @@
\]
as two inductive predicates.
If you think of \<open>a\<close> and \<open>b\<close> as ``\<open>(\<close>'' and ``\<open>)\<close>'',
-the grammar defines strings of balanced parentheses.
+the grammars define balanced strings of parentheses.
Prove \<^prop>\<open>T w \<Longrightarrow> S w\<close> and \mbox{\<^prop>\<open>S w \<Longrightarrow> T w\<close>} separately and conclude
\<^prop>\<open>S w = T w\<close>.
\end{exercise}