diff -r 1e80fc36776c -r 10264fe8012f src/Doc/Prog_Prove/Logic.thy
--- 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}