| Fri, 15 Dec 2000 17:59:05 +0100 | wenzelm | restore \int (integral); | changeset | files |
| Fri, 15 Dec 2000 17:58:40 +0100 | wenzelm | tuned symbols; | changeset | files |
| Fri, 15 Dec 2000 17:41:38 +0100 | paulson | further round of tidying | changeset | files |
| Fri, 15 Dec 2000 12:32:35 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 14 Dec 2000 19:38:37 +0100 | wenzelm | 'typedef': present result theorem "type_definition Rep Abs A"; | changeset | files |
| Thu, 14 Dec 2000 19:37:43 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 14 Dec 2000 19:37:27 +0100 | wenzelm | unsymbolize; | changeset | files |
| Thu, 14 Dec 2000 19:37:09 +0100 | wenzelm | use \<Sum> from main HOL; | changeset | files |
| Thu, 14 Dec 2000 19:36:48 +0100 | wenzelm | added Summation; | changeset | files |
| Thu, 14 Dec 2000 10:30:45 +0100 | paulson | many new proofs; still needs tidying | changeset | files |
| Thu, 14 Dec 2000 10:30:11 +0100 | paulson | new theorem real_lbound_gt_zero | changeset | files |
| Wed, 13 Dec 2000 17:46:49 +0100 | wenzelm | updated; | changeset | files |
| Wed, 13 Dec 2000 17:43:33 +0100 | wenzelm | eliminated GOAL syntax; | changeset | files |
| Wed, 13 Dec 2000 17:41:10 +0100 | wenzelm | fixed add_term_names: NameSpace.base; | changeset | files |
| Wed, 13 Dec 2000 16:22:10 +0100 | wenzelm | tuned comments; | changeset | files |
| Wed, 13 Dec 2000 16:21:40 +0100 | wenzelm | * print modes "brackets" and "no_brackets" control output of nested => | changeset | files |