src/HOL/ex/Sqrt_Script.thy

--- a/src/HOL/ex/Sqrt_Script.thy	Sat Jun 05 12:45:00 2021 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Sat Jun 05 12:57:52 2021 +0200
@@ -5,14 +5,14 @@
 
 section \<open>Square roots of primes are irrational (script version)\<close>
 
-theory Sqrt_Script
-imports Complex_Main "HOL-Computational_Algebra.Primes"
-begin
+text \<open>
+  Contrast this linear Isabelle/Isar script with the more mathematical version
+  in \<^file>\<open>~~/src/HOL/Examples/Sqrt.thy\<close> by Makarius Wenzel.
+\<close>
 
-text \<open>
-  \medskip Contrast this linear Isabelle/Isar script with Markus
-  Wenzel's more mathematical version.
-\<close>
+theory Sqrt_Script
+  imports Complex_Main "HOL-Computational_Algebra.Primes"
+begin
 
 subsection \<open>Preliminaries\<close>