Replaced blast by fast in proof of parts_singleton, since blast looped
authorberghofe
Wed May 07 10:59:02 2008 +0200 (2008-05-07)
changeset 268074cd176ea28dc
parent 26806 40b411ec05aa
child 26808 d334a6d69598
Replaced blast by fast in proof of parts_singleton, since blast looped
because of the new encoding of sets.
doc-src/TutorialI/Protocol/Message.thy
src/HOL/Auth/Message.thy
src/HOL/MetisExamples/Message.thy
src/HOL/SET-Protocol/MessageSET.thy
     1.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Wed May 07 10:57:19 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Wed May 07 10:59:02 2008 +0200
     1.3 @@ -204,7 +204,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 *}
     2.1 --- a/src/HOL/Auth/Message.thy	Wed May 07 10:57:19 2008 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Wed May 07 10:59:02 2008 +0200
     2.3 @@ -181,7 +181,7 @@
     2.4  
     2.5  text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
     2.6  lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
     2.7 -by (erule parts.induct, blast+)
     2.8 +by (erule parts.induct, fast+)
     2.9  
    2.10  
    2.11  subsubsection{*Unions *}
     3.1 --- a/src/HOL/MetisExamples/Message.thy	Wed May 07 10:57:19 2008 +0200
     3.2 +++ b/src/HOL/MetisExamples/Message.thy	Wed May 07 10:59:02 2008 +0200
     3.3 @@ -181,7 +181,7 @@
     3.4  text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
     3.5  lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
     3.6  apply (erule parts.induct)
     3.7 -apply blast+
     3.8 +apply fast+
     3.9  done
    3.10  
    3.11  
     4.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Wed May 07 10:57:19 2008 +0200
     4.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed May 07 10:59:02 2008 +0200
     4.3 @@ -225,7 +225,7 @@
     4.4  
     4.5  (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
     4.6  lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
     4.7 -by (erule parts.induct, blast+)
     4.8 +by (erule parts.induct, fast+)
     4.9  
    4.10  
    4.11  subsubsection{*Unions*}