--- a/ProgTutorial/Tactical.thy	Mon Nov 14 20:30:46 2011 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Nov 16 13:23:27 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 
@@ -2544,7 +2544,7 @@
 
 section {* Declarations (TBD) *}
 
-section {* Structured Proofs (TBD) *}
+section {* Structured Proofs\label{sec:structured} (TBD) *}
 
 text {* TBD *}