--- a/Tutorial/Tutorial3.thy	Sat Jan 22 16:04:40 2011 -0600
+++ b/Tutorial/Tutorial3.thy	Sat Jan 22 16:36:21 2011 -0600
@@ -5,16 +5,20 @@
 section {* Formalising Barendregt's Proof of the Substitution Lemma *}
 
 text {*
-  Barendregt's proof needs in the variable case a case distinction.
-  One way to do this in Isar is to use blocks. A block consist of some
-  assumptions and reasoning steps enclosed in curly braces, like
+  The substitution lemma is another theorem where the variable
+  convention plays a crucial role.
+
+  Barendregt's proof of this lemma needs in the variable case a 
+  case distinction. One way to do this in Isar is to use blocks. 
+  A block consist of some assumptions and reasoning steps 
+  enclosed in curly braces, like
 
   { \<dots>
     have "statement"
     have "last_statement_in_the_block"
   }
 
-  Such a block can contain local assumptions like
+  Such a block may contain local assumptions like
 
   { assume "A"
     assume "B"
@@ -74,7 +78,7 @@
 
 
 
-section {* EXERCISE 7 *}
+section {* EXERCISE 10 *}
 
 text {*
   Fill in the cases 1.2 and 1.3 and the equational reasoning 
@@ -143,5 +147,11 @@
 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
+subsection {* MINI EXERCISE *}
+
+text {*
+  Compare and contrast Barendregt's reasoning and the 
+  formalised proofs.
+*}
 
 end