--- a/src/HOL/Hyperreal/Filter.thy Wed Jan 02 15:14:20 2008 +0100
+++ b/src/HOL/Hyperreal/Filter.thy Wed Jan 02 15:14:22 2008 +0100
@@ -9,7 +9,7 @@
header {* Filters and Ultrafilters *}
theory Filter
-imports Zorn Infinite_Set
+imports "~~/src/HOL/Library/Zorn" "~~/src/HOL/Library/Infinite_Set"
begin
subsection {* Definitions and basic properties *}
--- a/src/HOL/Hyperreal/NthRoot.thy Wed Jan 02 15:14:20 2008 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy Wed Jan 02 15:14:22 2008 +0100
@@ -7,7 +7,7 @@
header {* Nth Roots of Real Numbers *}
theory NthRoot
-imports Parity "../Hyperreal/Deriv"
+imports "~~/src/HOL/Library/Parity" "../Hyperreal/Deriv"
begin
subsection {* Existence of Nth Root *}