# 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)