summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Primes.thy

changeset 26757 | e775accff967 |

parent 26159 | ff372ff5cc34 |

child 27106 | ff27dc6e7d05 |

1.1 --- a/src/HOL/Library/Primes.thy Mon Apr 28 14:42:13 2008 +0200 1.2 +++ b/src/HOL/Library/Primes.thy Mon Apr 28 20:21:11 2008 +0200 1.3 @@ -690,9 +690,9 @@ 1.4 let ?m = "Max ?P" 1.5 have P0: "?P \<noteq> {}" using two_is_prime by auto 1.6 from H have fP: "finite ?P" using finite_conv_nat_seg_image by blast 1.7 - from Max_in[OF fP P0] have "?m \<in> ?P" . 1.8 - from Max_ge[OF fP P0] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast 1.9 - from euclid[of ?m] obtain q where q: "prime q" "q > ?m" by blast 1.10 + from Max_in [OF fP P0] have "?m \<in> ?P" . 1.11 + from Max_ge [OF fP] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast 1.12 + from euclid [of ?m] obtain q where q: "prime q" "q > ?m" by blast 1.13 with contr show False by auto 1.14 qed 1.15 1.16 @@ -1045,4 +1045,5 @@ 1.17 1.18 declare power_Suc0[simp del] 1.19 declare even_dvd[simp del] 1.20 + 1.21 end