diff -r 7cdb86c8eb30 -r 6822aa82aafa src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Thu Feb 28 12:09:32 2013 +0100 +++ b/src/HOL/Library/Extended_Real.thy Thu Feb 28 12:24:24 2013 +0100 @@ -8,7 +8,7 @@ header {* Extended real number line *} theory Extended_Real -imports "~~/src/HOL/Complex_Main" Extended_Nat +imports Complex_Main Extended_Nat begin text {*