diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial4s.thy
--- a/Tutorial/Tutorial4s.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial4s.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -1,5 +1,5 @@
-theory Tutorial4
-imports Tutorial1
+theory Tutorial4s
+imports Tutorial1s
 begin
 
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -115,18 +115,22 @@
 proof (induct)
   case (m1 t1 t2 Es)
 thm machine.intros thm cbv2
-  have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
+  have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" 
+    using ctx_compose ctx_composes.simps filling.simps by simp
   then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp
 next
   case (m2 v t2 Es)
   have "val v" by fact
-  have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>"  using ctx_compose ctx_composes.simps filling.simps by simp
+  have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>"  
+    using ctx_compose ctx_composes.simps filling.simps by simp
   then show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using cbvs.intros by simp
 next
   case (m3 v x t Es)
   have aa: "val v" by fact
-  have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
-  then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using better_cbv1[OF aa] cbv_in_ctx by simp
+  have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" 
+    using ctx_compose ctx_composes.simps filling.simps by simp
+  then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" 
+    using better_cbv1[OF aa] cbv_in_ctx by simp
   then show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using cbvs.intros by blast
 qed