# HG changeset patch
# User wenzelm
# Date 1434572952 -7200
# Node ID 64d27b9f00a0ce73475542de32c6fc535f774d03
# Parent  0928cf63920f1c335ca2de2e81b4eefd72692aab
tuned proofs -- slightly faster;

diff -r 0928cf63920f -r 64d27b9f00a0 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Wed Jun 17 22:12:08 2015 +0200
+++ b/src/HOL/Library/Ramsey.thy	Wed Jun 17 22:29:12 2015 +0200
@@ -86,7 +86,7 @@
            by(auto simp:clique_def insert_commute)
           moreover have "card(insert v R) = m"
             using \<open>?C\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>m\<noteq>0\<close> by simp
-          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by blast
+          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset)
         } ultimately have "?EX V E m n" using CI by blast
       } moreover
       { assume "r2 \<le> card ?N"
@@ -106,7 +106,7 @@
             by(auto simp:indep_def insert_commute)
           moreover have "card(insert v R) = n"
             using \<open>?I\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>n\<noteq>0\<close> by simp
-          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by blast
+          ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset)
         } ultimately have "?EX V E m n" using CI by blast
       } ultimately show "?EX V E m n" by blast
     qed