# 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