minimize imports
authorhuffman
Wed May 16 23:03:45 2007 +0200 (2007-05-16)
changeset 229833314057c3b57
parent 22982 bff3fcdeecd3
child 22984 67d434ad9ef8
minimize imports
src/HOL/Complex/Complex_Main.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/Hyperreal.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Poly.thy
     1.1 --- a/src/HOL/Complex/Complex_Main.thy	Wed May 16 09:45:22 2007 +0200
     1.2 +++ b/src/HOL/Complex/Complex_Main.thy	Wed May 16 23:03:45 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header{*Comprehensive Complex Theory*}
     1.5  
     1.6  theory Complex_Main
     1.7 -imports CLim "../Hyperreal/HLog"
     1.8 +imports CLim "../Hyperreal/Hyperreal"
     1.9  begin
    1.10  
    1.11  end
     2.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Wed May 16 09:45:22 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed May 16 23:03:45 2007 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  header{*Nonstandard Extensions of Transcendental Functions*}
     2.5  
     2.6  theory HTranscendental
     2.7 -imports Transcendental Integration HSeries HDeriv
     2.8 +imports Transcendental HSeries HDeriv
     2.9  begin
    2.10  
    2.11  definition
     3.1 --- a/src/HOL/Hyperreal/Hyperreal.thy	Wed May 16 09:45:22 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Hyperreal.thy	Wed May 16 23:03:45 2007 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  *)
     3.5  
     3.6  theory Hyperreal
     3.7 -imports Poly Taylor HLog
     3.8 +imports Ln Poly Taylor Integration HLog
     3.9  begin
    3.10  
    3.11  end
     4.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed May 16 09:45:22 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed May 16 23:03:45 2007 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  header{*MacLaurin Series*}
     4.5  
     4.6  theory MacLaurin
     4.7 -imports Log
     4.8 +imports Transcendental
     4.9  begin
    4.10  
    4.11  subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
     5.1 --- a/src/HOL/Hyperreal/Poly.thy	Wed May 16 09:45:22 2007 +0200
     5.2 +++ b/src/HOL/Hyperreal/Poly.thy	Wed May 16 23:03:45 2007 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  header{*Univariate Real Polynomials*}
     5.5  
     5.6  theory Poly
     5.7 -imports Ln
     5.8 +imports Transcendental
     5.9  begin
    5.10  
    5.11  text{*Application of polynomial as a real function.*}