# HG changeset patch
# User wenzelm
# Date 1236700107 -3600
# Node ID 9c9b6511ad1b6a9d45ac636009f4c35b6b36abc0
# Parent  ef670320e281fc44371b11c5f63041c6cfc6f62c
tuned proofs;
tuned document;

diff -r ef670320e281 -r 9c9b6511ad1b src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Tue Mar 10 16:44:20 2009 +0100
+++ b/src/HOL/ex/Sqrt.thy	Tue Mar 10 16:48:27 2009 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/ex/Sqrt.thy
     Author:     Markus Wenzel, TU Muenchen
-
 *)
 
 header {*  Square roots of primes are irrational *}
@@ -9,13 +8,6 @@
 imports Complex_Main Primes
 begin
 
-text {* The definition and the key representation theorem for the set of
-rational numbers has been moved to a core theory.  *}
-
-declare Rats_abs_nat_div_natE[elim?]
-
-subsection {* Main theorem *}
-
 text {*
   The square root of any prime number (including @{text 2}) is
   irrational.
@@ -29,7 +21,7 @@
   assume "sqrt (real p) \<in> \<rat>"
   then obtain m n where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
-    and gcd: "gcd m n = 1" ..
+    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
   have eq: "m\<twosuperior> = p * n\<twosuperior>"
   proof -
     from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
@@ -75,7 +67,7 @@
   assume "sqrt (real p) \<in> \<rat>"
   then obtain m n where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
-    and gcd: "gcd m n = 1" ..
+    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
   from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
   then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
     by (auto simp add: power2_eq_square)