# HG changeset patch # User nipkow # Date 1151062939 -7200 # Node ID e3ddb08128406928f88329911469d329561505d8 # Parent ed388c5c7e54321f7ee8a9c5b3d6497739f448cf beautification diff -r ed388c5c7e54 -r e3ddb0812840 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Fri Jun 23 10:48:34 2006 +0200 +++ b/src/HOL/Library/Ramsey.thy Fri Jun 23 13:42:19 2006 +0200 @@ -25,7 +25,7 @@ proof (induct n) case 0 show ?case by (force intro: someI P0) next - case (Suc n) thus ?case by (auto intro: someI2_ex [OF Pstep]) + case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) qed lemma dependent_choice: @@ -125,10 +125,8 @@ qed qed from dependent_choice [OF transr propr0 proprstep] - obtain g where "(\n::nat. ?propr(g n)) & (\n m. n(g n, g m) \ ?ramr)" - .. --{*for some reason, can't derive the following directly from dc*} - hence pg: "!!n. ?propr (g n)" - and rg: "!!n m. n (g n, g m) \ ?ramr" by auto + obtain g where pg: "!!n::nat. ?propr (g n)" + and rg: "!!n m. n (g n, g m) \ ?ramr" by force let ?gy = "(\n. let (y,Y,t) = g n in y)" let ?gt = "(\n. let (y,Y,t) = g n in t)" have rangeg: "\k. range ?gt \ {.. AA"] fields cardX - by (clarify, drule_tac x="X-{ya}" in spec, simp) + by (clarsimp simp del:insert_Diff_single) qed also have "... = s'" using AA AAleast fields by auto finally show ?thesis . @@ -215,7 +213,7 @@ \X. X \ Z & finite X & card X = r --> f X < s|] ==> \Y t. Y \ Z & infinite Y & t < s & (\X. X \ Y & finite X & card X = r --> f X = t)" -by (blast intro: ramsey_induction [unfolded part_def, rule_format]) +by (blast intro: ramsey_induction [unfolded part_def]) end