# HG changeset patch # User huffman # Date 1179349425 -7200 # Node ID 3314057c3b575aa1e1adb03863da32ecc1c4e898 # Parent bff3fcdeecd38c3ffd0351239d94eb39902a2474 minimize imports diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Complex/Complex_Main.thy --- a/src/HOL/Complex/Complex_Main.thy Wed May 16 09:45:22 2007 +0200 +++ b/src/HOL/Complex/Complex_Main.thy Wed May 16 23:03:45 2007 +0200 @@ -7,7 +7,7 @@ header{*Comprehensive Complex Theory*} theory Complex_Main -imports CLim "../Hyperreal/HLog" +imports CLim "../Hyperreal/Hyperreal" begin end diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/HTranscendental.thy --- a/src/HOL/Hyperreal/HTranscendental.thy Wed May 16 09:45:22 2007 +0200 +++ b/src/HOL/Hyperreal/HTranscendental.thy Wed May 16 23:03:45 2007 +0200 @@ -8,7 +8,7 @@ header{*Nonstandard Extensions of Transcendental Functions*} theory HTranscendental -imports Transcendental Integration HSeries HDeriv +imports Transcendental HSeries HDeriv begin definition diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/Hyperreal.thy --- a/src/HOL/Hyperreal/Hyperreal.thy Wed May 16 09:45:22 2007 +0200 +++ b/src/HOL/Hyperreal/Hyperreal.thy Wed May 16 23:03:45 2007 +0200 @@ -8,7 +8,7 @@ *) theory Hyperreal -imports Poly Taylor HLog +imports Ln Poly Taylor Integration HLog begin end diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Wed May 16 09:45:22 2007 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Wed May 16 23:03:45 2007 +0200 @@ -7,7 +7,7 @@ header{*MacLaurin Series*} theory MacLaurin -imports Log +imports Transcendental begin subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} diff -r bff3fcdeecd3 -r 3314057c3b57 src/HOL/Hyperreal/Poly.thy --- a/src/HOL/Hyperreal/Poly.thy Wed May 16 09:45:22 2007 +0200 +++ b/src/HOL/Hyperreal/Poly.thy Wed May 16 23:03:45 2007 +0200 @@ -9,7 +9,7 @@ header{*Univariate Real Polynomials*} theory Poly -imports Ln +imports Transcendental begin text{*Application of polynomial as a real function.*}