src/Doc/Prog_Prove/Logic.thy

--- a/src/Doc/Prog_Prove/Logic.thy	Mon Aug 24 00:20:20 2015 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy	Mon Aug 24 16:19:47 2015 +0200
@@ -826,7 +826,7 @@
 @{prop"star r x y \<Longrightarrow> iter r n x y"}.
 \end{exercise}
 
-\begin{exercise}
+\begin{exercise}\label{exe:cfg}
 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)$ means that $w$ is in the language generated by $A$.