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