| changeset 26807 | 4cd176ea28dc |
| parent 25341 | ca3761e38a87 |
| child 27147 | 62ab1968c1f4 |
--- a/doc-src/TutorialI/Protocol/Message.thy Wed May 07 10:57:19 2008 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Wed May 07 10:59:02 2008 +0200 @@ -204,7 +204,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 *}