changeset 44890 | 22f665a2e91c |
parent 39779 | 863362a2d865 |
child 45966 | 03ce2b2a29a2 |
--- a/src/HOL/Nominal/Examples/Standardization.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Nominal/Examples/Standardization.thy Mon Sep 12 07:55:43 2011 +0200 @@ -296,7 +296,7 @@ apply (erule exE) apply (rename_tac ts) apply (case_tac ts) - apply fastsimp + apply fastforce apply force apply (erule disjE) apply blast