| Fri, 19 Aug 2011 17:59:19 -0700 | huffman | remove redundant lemma exp_ln_eq in favor of ln_unique | file | diff | annotate |
| Mon, 19 Jul 2010 16:09:44 +0200 | haftmann | diff_minus subsumes diff_def | file | diff | annotate |
| Wed, 27 May 2009 16:39:22 -0700 | huffman | add constants sin_coeff, cos_coeff | file | diff | annotate |
| Wed, 04 Mar 2009 17:12:23 -0800 | huffman | declare power_Suc [simp]; remove redundant type-specific versions of power_Suc | file | diff | annotate |
| Thu, 03 Jul 2008 17:47:22 +0200 | huffman | move nonstandard analysis theories to NSA directory | file | diff | annotate |