# HG changeset patch
# User nipkow
# Date 1092911745 -7200
# Node ID c5c4884634b7e4783e9b90e1bcf2c8c42b29e5dc
# Parent  3879dc0e9a9c701f6bdc4ab407715efb8a98ab80
new import syntax

diff -r 3879dc0e9a9c -r c5c4884634b7 src/HOL/Complex/ex/BinEx.thy
--- 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
diff -r 3879dc0e9a9c -r c5c4884634b7 src/HOL/Complex/ex/NSPrimes.thy
--- 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.*}
diff -r 3879dc0e9a9c -r c5c4884634b7 src/HOL/Complex/ex/Sqrt.thy
--- 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 *}
 
diff -r 3879dc0e9a9c -r c5c4884634b7 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