diff -r 3778bddfb824 -r 1d1165432c9f ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Nov 24 19:54:01 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Fri Nov 25 00:27:05 2011 +0000
@@ -23,7 +23,7 @@
   tactic combinators. We also describe the simplifier, simprocs and conversions.
 *}
 
-section {* Basics of Reasoning with Tactics*}
+section {* Basics of Reasoning with Tactics\label{sec:basictactics}*}
 
 text {*
   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
@@ -2543,7 +2543,7 @@
 
 section {* Declarations (TBD) *}
 
-section {* Structured Proofs (TBD) *}
+section {* Structured Proofs\label{sec:structured} (TBD) *}
 
 text {* TBD *}