# HG changeset patch
# User wenzelm
# Date 1005088579 -3600
# Node ID b38cfbabfda4da51845db9fbe2e02e52500b6274
# Parent  742b9c3740dcb2ba4a677d7545ddc24a47cb266b
tuned;

diff -r 742b9c3740dc -r b38cfbabfda4 src/HOL/Real/ex/Sqrt_Script.thy
--- a/src/HOL/Real/ex/Sqrt_Script.thy	Tue Nov 06 23:56:14 2001 +0100
+++ b/src/HOL/Real/ex/Sqrt_Script.thy	Wed Nov 07 00:16:19 2001 +0100
@@ -13,7 +13,7 @@
   mathematical version.
 *}
 
-section {* Preliminaries *}
+subsection {* Preliminaries *}
 
 lemma prime_nonzero:  "p \<in> prime \<Longrightarrow> p\<noteq>0"
 by (force simp add: prime_def)
@@ -46,14 +46,14 @@
 done
 
 
-section {* The set of rational numbers [Borrowed from Markus Wenzel] *}
+subsection {* The set of rational numbers *}
 
 constdefs
   rationals :: "real set"    ("\<rat>")
   "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
 
 
-section {* Main theorem *}
+subsection {* Main theorem *}
 
 text {*
   The square root of any prime number (including @{text 2}) is