diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/CPS/CPS1_Plotkin.thy --- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Thu Mar 13 09:30:26 2014 +0000 +++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon Mar 24 15:31:17 2014 +0000 @@ -86,7 +86,6 @@ apply (erule lt.exhaust) using [[simproc del: alpha_lst]] apply (simp_all) - apply blast apply (simp add: Abs1_eq_iff CPS.eqvt) by blast