# HG changeset patch
# User haftmann
# Date 1199283262 -3600
# Node ID 6960410f134dacd83fc076dbae88cbbedf443e1a
# Parent  49580bd58a21a240e456d5aa881c37698a9e5010
absolute import

diff -r 49580bd58a21 -r 6960410f134d src/HOL/Hyperreal/Filter.thy
--- 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 *}
diff -r 49580bd58a21 -r 6960410f134d src/HOL/Hyperreal/NthRoot.thy
--- 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 *}