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