# HG changeset patch
# User nipkow
# Date 1363598922 -3600
# Node ID 1c9538a04e639bd77f4f7e59caeb6585e293be87
# Parent  027cdce376d50227683cff40d3788f337141de67
tuned

diff -r 027cdce376d5 -r 1c9538a04e63 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}