--- a/src/HOL/Complex/ex/BinEx.thy Thu Aug 19 10:33:10 2004 +0200
+++ b/src/HOL/Complex/ex/BinEx.thy Thu Aug 19 12:35:45 2004 +0200
@@ -6,7 +6,9 @@
header {* Binary arithmetic examples *}
-theory BinEx = Complex_Main:
+theory BinEx
+imports Complex_Main
+begin
text {*
Examples of performing binary arithmetic by simplification. This time
--- a/src/HOL/Complex/ex/NSPrimes.thy Thu Aug 19 10:33:10 2004 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy Thu Aug 19 12:35:45 2004 +0200
@@ -6,7 +6,9 @@
header{*The Nonstandard Primes as an Extension of the Prime Numbers*}
-theory NSPrimes = "~~/src/HOL/NumberTheory/Factorization" + Complex_Main:
+theory NSPrimes
+imports "~~/src/HOL/NumberTheory/Factorization" Complex_Main
+begin
text{*These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.*}
--- a/src/HOL/Complex/ex/Sqrt.thy Thu Aug 19 10:33:10 2004 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy Thu Aug 19 12:35:45 2004 +0200
@@ -6,7 +6,9 @@
header {* Square roots of primes are irrational *}
-theory Sqrt = Primes + Complex_Main:
+theory Sqrt
+imports Primes Complex_Main
+begin
subsection {* Preliminaries *}
--- 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