# HG changeset patch
# User berghofe
# Date 1210150742 -7200
# Node ID 4cd176ea28dcc488733aed807ae477a69cf64186
# Parent  40b411ec05aadaa7858b76c524fa42acc42f1029
Replaced blast by fast in proof of parts_singleton, since blast looped
because of the new encoding of sets.

diff -r 40b411ec05aa -r 4cd176ea28dc doc-src/TutorialI/Protocol/Message.thy
--- 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 *}
diff -r 40b411ec05aa -r 4cd176ea28dc src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed May 07 10:57:19 2008 +0200
+++ b/src/HOL/Auth/Message.thy	Wed May 07 10:59:02 2008 +0200
@@ -181,7 +181,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 *}
diff -r 40b411ec05aa -r 4cd176ea28dc src/HOL/MetisExamples/Message.thy
--- a/src/HOL/MetisExamples/Message.thy	Wed May 07 10:57:19 2008 +0200
+++ b/src/HOL/MetisExamples/Message.thy	Wed May 07 10:59:02 2008 +0200
@@ -181,7 +181,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}"
 apply (erule parts.induct)
-apply blast+
+apply fast+
 done
 
 
diff -r 40b411ec05aa -r 4cd176ea28dc src/HOL/SET-Protocol/MessageSET.thy
--- 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*}