--- a/ProgTutorial/Tactical.thy	Wed Oct 07 09:54:01 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Oct 07 11:28:40 2009 +0200
@@ -2206,7 +2206,7 @@
 where "id2 \<equiv> \<lambda>x. x"
 
 text {*
-  Both definitions define the same function, although the theorems @{thm
+  Although both definitions define the same function, the theorems @{thm
   [source] id1_def} and @{thm [source] id2_def} are different. However it is
   easy to transform one theorem into the other. The function @{ML_ind abs_def
   in Drule} can automatically transform theorem @{thm [source] id1_def}