--- a/src/HOL/Real/ex/Sqrt_Irrational.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/ex/Sqrt_Irrational.thy Sat Oct 06 00:02:46 2001 +0200
@@ -114,15 +114,15 @@
this formally :-).
*}
-theorem "x\<twosuperior> = real (# 2::nat) ==> x \<notin> \<rat>"
+theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>"
proof (rule sqrt_prime_irrational)
{
- fix m :: nat assume dvd: "m dvd # 2"
- hence "m \<le> # 2" by (simp add: dvd_imp_le)
+ fix m :: nat assume dvd: "m dvd 2"
+ hence "m \<le> 2" by (simp add: dvd_imp_le)
moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
- ultimately have "m = 1 \<or> m = # 2" by arith
+ ultimately have "m = 1 \<or> m = 2" by arith
}
- thus "# 2 \<in> prime" by (simp add: prime_def)
+ thus "2 \<in> prime" by (simp add: prime_def)
qed
text {*