--- a/Tutorial/Tutorial3.thy	Fri Jan 21 22:02:34 2011 +0100
+++ b/Tutorial/Tutorial3.thy	Fri Jan 21 22:23:44 2011 +0100
@@ -6,12 +6,12 @@
 
 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 is some sequent
-  or reasoning steps enclosed in curly braces
+  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
@@ -25,7 +25,7 @@
   Where "C" is the last have-statement in this block. The behaviour 
   of such a block to the 'outside' is the implication
 
-   \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C" 
+   A \<Longrightarrow> B \<Longrightarrow> C 
 
   Now if we want to prove a property "smth" using the case-distinctions
   P1, P2 and P3 then we can use the following reasoning:
@@ -52,17 +52,12 @@
     P2 \<Longrightarrow> smth
     P3 \<Longrightarrow> smth
 
-  If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 is
-  true, then we have 'ultimately' established the property "smth" 
+  If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 
+  holds, then we have 'ultimately' established the property "smth" 
   
 *}
 
-section {* EXERCISE 7 *}
-
-text {*
-  Fill in the cases 1.2 and 1.3 and the equational reasoning 
-  in the lambda-case.
-*}
+subsection {* Two preliminary facts *}
 
 lemma forget:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
@@ -78,6 +73,14 @@
    (auto simp add: lam.fresh fresh_at_base)
 
 
+
+section {* EXERCISE 7 *}
+
+text {*
+  Fill in the cases 1.2 and 1.3 and the equational reasoning 
+  in the lambda-case.
+*}
+
 lemma 
   assumes a: "x \<noteq> y"
   and     b: "atom x \<sharp> L"
@@ -111,12 +114,12 @@
   qed
 next
   case (Lam z M1) -- {* case 2: lambdas *}
-  have ih: "\<lbrakk>x \<noteq> y; atom x \<sharp> L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
+  have ih: "\<lbrakk>x \<noteq> y; atom x \<sharp> L\<rbrakk> \<Longrightarrow> M1[x ::= N][y ::= L] = M1[y ::= L][x ::= N[y ::= L]]" by fact
   have a1: "x \<noteq> y" by fact
   have a2: "atom x \<sharp> L" by fact
-  have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+
+  have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+   -- {* !! *}
   then have b: "atom z \<sharp> N[y::=L]" by (simp add: fresh_fact)
-  show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
+  show "(Lam [z].M1)[x ::= N][y ::= L] = (Lam [z].M1)[y ::= L][x ::= N[y ::= L]]" (is "?LHS=?RHS") 
   proof - 
     have "?LHS = \<dots>" sorry
 
@@ -130,7 +133,7 @@
 
 text {* 
   Again the strong induction principle enables Isabelle to find
-  the proof of the substitution lemma automatically. 
+  the proof of the substitution lemma completely automatically. 
 *}
 
 lemma substitution_lemma_version: