# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1404814711 -3600
# Node ID b2e1a7b83e05d5f9f201297d9c828460bc271965
# Parent  8ee8f72778cea2c948413e1a41cc34038791a79b
updated for 2014 release

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)