| changeset 26807 | 4cd176ea28dc |
| parent 26342 | 0f65fa163304 |
| child 27147 | 62ab1968c1f4 |
--- a/src/HOL/SET-Protocol/MessageSET.thy Wed May 07 10:57:19 2008 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Wed May 07 10:59:02 2008 +0200 @@ -225,7 +225,7 @@ (*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*}