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