src/Doc/ProgProve/Isar.thy

--- a/src/Doc/ProgProve/Isar.thy	Sun Mar 17 20:29:26 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Mon Mar 18 10:28:42 2013 +0100
@@ -981,6 +981,7 @@
 prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}
 
 \subsection{Advanced rule induction}
+\label{sec:advanced-rule-induction}
 
 So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}
 where @{text I} is some inductively defined predicate and @{text x}, @{text y}, @{text z}