src/HOL/Complex/ex/Sqrt_Script.thy

--- a/src/HOL/Complex/ex/Sqrt_Script.thy	Thu Aug 19 10:33:10 2004 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Thu Aug 19 12:35:45 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Square roots of primes are irrational (script version) *}
 
-theory Sqrt_Script = Primes + Complex_Main:
+theory Sqrt_Script
+imports Primes Complex_Main
+begin
 
 text {*
   \medskip Contrast this linear Isabelle/Isar script with Markus