# HG changeset patch
# User wenzelm
# Date 1010952891 -3600
# Node ID c06aee15dc00ed2c5bc2e24bedb33df2fbfcda73
# Parent  4e45fb10c811a6c37ee3cd3b30d6f9c9ca7c8502
\<twosuperior> syntax moved to HOL/Numerals;

diff -r 4e45fb10c811 -r c06aee15dc00 src/HOL/Real/ex/Sqrt.thy
--- a/src/HOL/Real/ex/Sqrt.thy	Sun Jan 13 21:14:31 2002 +0100
+++ b/src/HOL/Real/ex/Sqrt.thy	Sun Jan 13 21:14:51 2002 +0100
@@ -8,16 +8,6 @@
 
 theory Sqrt = Primes + Real:
 
-syntax (xsymbols)                        (* FIXME move to main HOL (!?) *)
-  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
-syntax (HTML output)
-  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
-syntax (output)
-  "_square" :: "'a => 'a"  ("(_^2)" [1000] 999)
-translations
-  "x\<twosuperior>" == "x^Suc (Suc 0)"
-
-
 subsection {* The set of rational numbers *}
 
 constdefs
@@ -86,19 +76,20 @@
   have eq: "m\<twosuperior> = p * n\<twosuperior>"
   proof -
     from n x_rat have "real m = \<bar>x\<bar> * real n" by simp
-    hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)" by (simp split: abs_split)
+    hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)"
+      by (simp add: power_two real_power_two split: abs_split)
     also from x_sqrt have "... = real (p * n\<twosuperior>)" by simp
     finally show ?thesis ..
   qed
   have "p dvd m \<and> p dvd n"
   proof
     from eq have "p dvd m\<twosuperior>" ..
-    with p_prime show "p dvd m" by (rule prime_dvd_square)
+    with p_prime show "p dvd m" by (rule prime_dvd_power_two)
     then obtain k where "m = p * k" ..
-    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: mult_ac)
-    with p have "n\<twosuperior> = p * k\<twosuperior>" by simp
+    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
+    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
     hence "p dvd n\<twosuperior>" ..
-    with p_prime show "p dvd n" by (rule prime_dvd_square)
+    with p_prime show "p dvd n" by (rule prime_dvd_power_two)
   qed
   hence "p dvd gcd (m, n)" ..
   with gcd have "p dvd 1" by simp
@@ -141,16 +132,17 @@
   then obtain m n where
     n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" and gcd: "gcd (m, n) = 1" ..
   from n x_rat have "real m = \<bar>x\<bar> * real n" by simp
-  hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)" by (simp split: abs_split)
+  hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)"
+    by (simp add: power_two real_power_two split: abs_split)
   also from x_sqrt have "... = real (p * n\<twosuperior>)" by simp
   finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
   hence "p dvd m\<twosuperior>" ..
-  with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_square)
+  with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
   then obtain k where "m = p * k" ..
-  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: mult_ac)
-  with p have "n\<twosuperior> = p * k\<twosuperior>" by simp
+  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
+  with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
   hence "p dvd n\<twosuperior>" ..
-  with p_prime have "p dvd n" by (rule prime_dvd_square)
+  with p_prime have "p dvd n" by (rule prime_dvd_power_two)
   with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
   with gcd have "p dvd 1" by simp
   hence "p \<le> 1" by (simp add: dvd_imp_le)