equal
deleted
inserted
replaced
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
6 *) |
6 *) |
7 |
7 |
8 header{*Power Series, Transcendental Functions etc.*} |
8 header{*Power Series, Transcendental Functions etc.*} |
9 |
9 |
10 theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim: |
10 theory Transcendental |
|
11 import NthRoot Fact HSeries EvenOdd Lim |
|
12 begin |
11 |
13 |
12 constdefs |
14 constdefs |
13 root :: "[nat,real] => real" |
15 root :: "[nat,real] => real" |
14 "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))" |
16 "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))" |
15 |
17 |