
diff -r 8ee8f72778ce -r b2e1a7b83e05 Tutorial/Tutorial5.thy
--- a/Tutorial/Tutorial5.thy	Mon Jul 07 10:21:40 2014 +0100
+++ b/Tutorial/Tutorial5.thy	Tue Jul 08 11:18:31 2014 +0100
@@ -128,9 +128,8 @@
 using ty fc
 apply(cases)
 using [[simproc del: alpha_lst]]
-apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
 apply(auto simp add: Abs1_eq_iff)
-apply(rotate_tac 3)
+apply(rotate_tac 4)
 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
 apply(perm_simp)
 apply(auto simp add: flip_fresh_fresh ty_fresh)




