| Tue, 16 Oct 2001 17:51:12 +0200 |
wenzelm |
* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 00:50:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 00:39:34 +0200 |
wenzelm |
improved induct;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 21:04:46 +0200 |
kleing |
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
|
file |
diff |
annotate
|
| Sat, 13 Oct 2001 21:45:23 +0200 |
wenzelm |
* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2001 20:30:38 +0200 |
wenzelm |
* Pure: added 'corollary' command;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2001 21:25:45 +0200 |
wenzelm |
* Isar/Pure: fixed 'token_translation' command;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2001 14:30:28 +0200 |
wenzelm |
* added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 23:58:17 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:50:37 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 16:07:43 +0200 |
wenzelm |
improved proof by cases and induction;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 11:28:30 +0200 |
wenzelm |
* moved induct/cases attributes to Pure, added 'print_induct_rules' command;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 20:58:27 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 19:23:58 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:30:09 +0200 |
wenzelm |
HOL: eliminated global items;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2001 22:24:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 08 Sep 2001 20:02:09 +0200 |
wenzelm |
* system: support Poly/ML 4.1.1 (large heaps);
|
file |
diff |
annotate
|
| Tue, 04 Sep 2001 21:10:57 +0200 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 22:46:23 +0200 |
wenzelm |
* Proof General keywords specification is now part of the Isabelle
|
file |
diff |
annotate
|
| Thu, 09 Aug 2001 10:16:23 +0200 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| Wed, 08 Aug 2001 17:37:47 +0200 |
wenzelm |
* HOL: syntax translations now work properly with numerals and records
|
file |
diff |
annotate
|
| Tue, 07 Aug 2001 22:42:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2001 22:41:46 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2001 22:02:45 +0200 |
wenzelm |
HOL: added "The";
|
file |
diff |
annotate
|
| Tue, 03 Jul 2001 15:40:25 +0200 |
paulson |
GroupTheory
|
file |
diff |
annotate
|
| Tue, 05 Jun 2001 09:51:04 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 21 May 2001 12:51:15 +0200 |
paulson |
ZF: division
|
file |
diff |
annotate
|
| Fri, 18 May 2001 12:13:53 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 09 Apr 2001 10:10:21 +0200 |
paulson |
Isar hint
|
file |
diff |
annotate
|
| Fri, 23 Feb 2001 16:31:21 +0100 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|