equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header{*Nonstandard Extensions of Transcendental Functions*} |
8 header{*Nonstandard Extensions of Transcendental Functions*} |
9 |
9 |
10 theory HTranscendental |
10 theory HTranscendental |
11 imports Transcendental Integration |
11 imports Transcendental Integration HSeries |
12 begin |
12 begin |
13 |
13 |
14 text{*really belongs in Transcendental*} |
14 text{*really belongs in Transcendental*} |
15 lemma sqrt_divide_self_eq: |
15 lemma sqrt_divide_self_eq: |
16 assumes nneg: "0 \<le> x" |
16 assumes nneg: "0 \<le> x" |