--- 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
--- 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
--- 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"