changeset 22983 | 3314057c3b57 |
parent 22859 | c03c076d9dca |
child 23096 | 423ad2fe9f76 |
--- 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