--- a/Tutorial/Tutorial1s.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial1s.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -678,7 +678,7 @@
 
 text {* Complete the proof and remove the sorries. *}
 
-lemma
+lemma ctx_compose:
   shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
 proof (induct E1)
   case Hole