summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 17 Jun 2015 22:29:12 +0200 | |

changeset 60510 | 64d27b9f00a0 |

parent 60509 | 0928cf63920f |

child 60511 | 5e67a223a141 |

tuned proofs -- slightly faster;

--- 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