1.1 --- a/src/HOL/Real/ex/Sqrt_Irrational.thy	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Real/ex/Sqrt_Irrational.thy	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -114,15 +114,15 @@
     1.4    this formally :-).
     1.5  *}
     1.6  
     1.7 -theorem "x\<twosuperior> = real (# 2::nat) ==> x \<notin> \<rat>"
     1.8 +theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>"
     1.9  proof (rule sqrt_prime_irrational)
    1.10    {
    1.11 -    fix m :: nat assume dvd: "m dvd # 2"
    1.12 -    hence "m \<le> # 2" by (simp add: dvd_imp_le)
    1.13 +    fix m :: nat assume dvd: "m dvd 2"
    1.14 +    hence "m \<le> 2" by (simp add: dvd_imp_le)
    1.15      moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
    1.16 -    ultimately have "m = 1 \<or> m = # 2" by arith
    1.17 +    ultimately have "m = 1 \<or> m = 2" by arith
    1.18    }
    1.19 -  thus "# 2 \<in> prime" by (simp add: prime_def)
    1.20 +  thus "2 \<in> prime" by (simp add: prime_def)
    1.21  qed
    1.22  
    1.23  text {*