diff options
| author | Larry D. Lee Jr | 2020-06-18 19:11:47 -0400 |
|---|---|---|
| committer | Larry D. Lee Jr | 2020-07-05 12:59:08 -0400 |
| commit | 50b0b8f2f8c02c4866a0ee0e88835232d5535c2d (patch) | |
| tree | c062fb54ff1b8d4177a067838596574225a564de /lib/objFile.ml | |
| parent | 0545c9402310efe0656793197c996d04d554ecb8 (diff) | |
Defined arbitrary base logarithms (Rlog) and added natural lemmas concerning ln, exp, and Rlog to the Real library. Additionally made the real exponent notation nonlocal.
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions