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