diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Wed Oct 18 17:19:18 2000 +0200
@@ -1,8 +1,8 @@
 (*<*)theory AB = Main:(*>*)
 
-section{*A context free grammar*}
+section{*Case study: A context free grammar*}
 
-text{*
+text{*\label{sec:CFG}
 Grammars are nothing but shorthands for inductive definitions of nonterminals
 which represent sets of strings. For example, the production
 $A \to B c$ is short for
@@ -43,7 +43,8 @@
 
 text{*\noindent
 The above productions are recast as a \emph{simultaneous} inductive
-definition of @{term S}, @{term A} and @{term B}:
+definition\index{inductive definition!simultaneous}
+of @{term S}, @{term A} and @{term B}:
 *}
 
 inductive S A B