changeset 67006 | b1278ed3cd46 |
parent 66453 | cc19f7ca2ed6 |
child 67091 | 1393c2340eec |
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sat Nov 04 18:57:49 2017 +0100 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy Sat Nov 04 19:17:19 2017 +0100 @@ -8,7 +8,7 @@ section\<open>Nonstandard Extensions of Transcendental Functions\<close> theory HTranscendental -imports HOL.Transcendental HSeries HDeriv +imports Complex_Main HSeries HDeriv begin definition