# HG changeset patch
# User haftmann
# Date 1215759743 -7200
# Node ID 9e585e99b494284dfd48d30acce25b38a18817f7
# Parent  dc38e79f5a1c6dd10856f715cf2da6e26140b648
tuned import

diff -r dc38e79f5a1c -r 9e585e99b494 src/HOL/Algebra/abstract/Abstract.thy
--- a/src/HOL/Algebra/abstract/Abstract.thy	Fri Jul 11 09:02:22 2008 +0200
+++ b/src/HOL/Algebra/abstract/Abstract.thy	Fri Jul 11 09:02:23 2008 +0200
@@ -4,6 +4,8 @@
     Author: Clemens Ballarin, started 17 July 1997
 *)
 
-theory Abstract imports RingHomo Field begin
+theory Abstract
+imports RingHomo Field
+begin
 
 end
diff -r dc38e79f5a1c -r 9e585e99b494 src/HOL/Algebra/abstract/RingHomo.thy
--- a/src/HOL/Algebra/abstract/RingHomo.thy	Fri Jul 11 09:02:22 2008 +0200
+++ b/src/HOL/Algebra/abstract/RingHomo.thy	Fri Jul 11 09:02:23 2008 +0200
@@ -6,7 +6,9 @@
 
 header {* Ring homomorphism *}
 
-theory RingHomo imports Ring2 begin
+theory RingHomo
+imports Ring2
+begin
 
 definition
   homo :: "('a::ring => 'b::ring) => bool" where
diff -r dc38e79f5a1c -r 9e585e99b494 src/HOL/Complex/Complex_Main.thy
--- a/src/HOL/Complex/Complex_Main.thy	Fri Jul 11 09:02:22 2008 +0200
+++ b/src/HOL/Complex/Complex_Main.thy	Fri Jul 11 09:02:23 2008 +0200
@@ -8,7 +8,7 @@
 
 theory Complex_Main
 imports
-  Main
+  "../Main"
   Fundamental_Theorem_Algebra
   "../Hyperreal/Log"
   "../Hyperreal/Ln"