src/HOL/Complex/ex/Sqrt_Script.thy

--- a/src/HOL/Complex/ex/Sqrt_Script.thy	Wed May 28 10:47:54 2003 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Wed May 28 10:48:20 2003 +0200
@@ -6,7 +6,7 @@
 
 header {* Square roots of primes are irrational (script version) *}
 
-theory Sqrt_Script = Primes + Hyperreal:
+theory Sqrt_Script = Primes + Complex_Main:
 
 text {*
   \medskip Contrast this linear Isabelle/Isar script with Markus