| changeset 26807 | 4cd176ea28dc |
| parent 26342 | 0f65fa163304 |
| child 27105 | 5f139027c365 |
--- a/src/HOL/Auth/Message.thy Wed May 07 10:57:19 2008 +0200 +++ b/src/HOL/Auth/Message.thy Wed May 07 10:59:02 2008 +0200 @@ -181,7 +181,7 @@ text{*WARNING: loops if H = {Y}, therefore must not be repeated!*} lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}" -by (erule parts.induct, blast+) +by (erule parts.induct, fast+) subsubsection{*Unions *}