| changeset 61975 | b4b11391c676 |
| parent 61945 | 1135b8de26c3 |
| child 61981 | 1b5845c62fa0 |
| 61974:5b067c681989 | 61975:b4b11391c676 |
|---|---|
1 (* Title : HLog.thy |
1 (* Title : HLog.thy |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 2000,2001 University of Edinburgh |
3 Copyright : 2000,2001 University of Edinburgh |
4 *) |
4 *) |
5 |
5 |
6 section{*Logarithms: Non-Standard Version*} |
6 section\<open>Logarithms: Non-Standard Version\<close> |
7 |
7 |
8 theory HLog |
8 theory HLog |
9 imports HTranscendental |
9 imports HTranscendental |
10 begin |
10 begin |
11 |
11 |