| changeset 51301 | 6822aa82aafa |
| parent 51022 | 78de6c7e8a58 |
| child 51328 | d63ec23c9125 |
--- 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 {*