# HG changeset patch
# User haftmann
# Date 1222084561 -7200
# Node ID 1742947952f829ef7dbc32a746dfeea3e34ed4f2
# Parent  f0838044f034379aeeaf860ba0bb6067f759d2af
absolute Library path

diff -r f0838044f034 -r 1742947952f8 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Mon Sep 22 13:55:59 2008 +0200
+++ b/src/HOL/Code_Eval.thy	Mon Sep 22 13:56:01 2008 +0200
@@ -6,7 +6,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Eval
-imports Plain RType
+imports Plain "~~/src/HOL/Library/RType"
 begin
 
 subsection {* Term representation *}
diff -r f0838044f034 -r 1742947952f8 src/HOL/Complex/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Mon Sep 22 13:55:59 2008 +0200
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Mon Sep 22 13:56:01 2008 +0200
@@ -6,7 +6,7 @@
 header{*Fundamental Theorem of Algebra*}
 
 theory Fundamental_Theorem_Algebra
-imports Univ_Poly Dense_Linear_Order Complex
+imports "~~/src/HOL/Library/Univ_Poly" "~~/src/HOL/Library/Dense_Linear_Order" Complex
 begin
 
 subsection {* Square root of complex numbers *}
diff -r f0838044f034 -r 1742947952f8 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Mon Sep 22 13:55:59 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Mon Sep 22 13:56:01 2008 +0200
@@ -6,7 +6,7 @@
 header {* Rational numbers *}
 
 theory Rational
-imports "../Nat_Int_Bij" GCD
+imports "../Nat_Int_Bij" "~~/src/HOL/Library/GCD"
 uses ("rat_arith.ML")
 begin