equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section\<open>Nonstandard Extensions of Transcendental Functions\<close> |
8 section\<open>Nonstandard Extensions of Transcendental Functions\<close> |
9 |
9 |
10 theory HTranscendental |
10 theory HTranscendental |
11 imports HOL.Transcendental HSeries HDeriv |
11 imports Complex_Main HSeries HDeriv |
12 begin |
12 begin |
13 |
13 |
14 definition |
14 definition |
15 exphr :: "real => hypreal" where |
15 exphr :: "real => hypreal" where |
16 \<comment>\<open>define exponential function using standard part\<close> |
16 \<comment>\<open>define exponential function using standard part\<close> |