| Thu, 30 Apr 2015 15:28:01 +0100 |
paulson |
tidying some messy proofs
|
changeset |
files
|
| Fri, 01 May 2015 08:45:30 +0200 |
nipkow |
new simp rule
|
changeset |
files
|
| Thu, 30 Apr 2015 16:07:43 +0200 |
wenzelm |
more formal source, more PIDE markup;
|
changeset |
files
|
| Thu, 30 Apr 2015 15:58:15 +0200 |
wenzelm |
tuned -- avoid odd rebinding of "ctxt" and "context";
|
changeset |
files
|
| Thu, 30 Apr 2015 15:41:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 29 Apr 2015 23:30:47 +0200 |
wenzelm |
use smaller example that fits into 64MB string limit of Poly/ML x86 platform;
|
changeset |
files
|
| Wed, 29 Apr 2015 23:26:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 29 Apr 2015 14:04:22 +0100 |
paulson |
Tidying. Improved simplification for numerals, esp in exponents.
|
changeset |
files
|
| Tue, 28 Apr 2015 22:57:07 +0200 |
blanchet |
allow sorts on dead variables in BNFs
|
changeset |
files
|
| Tue, 28 Apr 2015 22:56:50 +0200 |
blanchet |
added known bug
|
changeset |
files
|
| Tue, 28 Apr 2015 22:56:28 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 28 Apr 2015 19:09:28 +0200 |
nipkow |
undid 6d7b7a037e8d
|
changeset |
files
|
| Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
changeset |
files
|
| Tue, 28 Apr 2015 16:23:05 +0100 |
paulson |
Fixed a non-terminating proof (almost certainly caused by no change of mind)
|
changeset |
files
|