| changeset 56073 | 29e308b56d23 |
| parent 55414 | eab03e9cee8a |
| child 57492 | 74bf65a1910a |
--- a/src/HOL/Nominal/Examples/Class2.thy Wed Mar 12 22:57:50 2014 +0100 +++ b/src/HOL/Nominal/Examples/Class2.thy Thu Mar 13 07:07:07 2014 +0100 @@ -2869,15 +2869,9 @@ apply(rotate_tac 10) apply(drule_tac x="a" in meta_spec) apply(auto simp add: ty.inject) -apply(blast) -apply(blast) -apply(blast) apply(rotate_tac 10) apply(drule_tac x="a" in meta_spec) apply(auto simp add: ty.inject) -apply(blast) -apply(blast) -apply(blast) done termination