| Thu, 25 Oct 2001 22:42:12 +0200 |
wenzelm |
* HOL/record:
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 22:41:07 +0200 |
wenzelm |
* Provers: 'simplified' attribute may refer to explicit rules instead
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 19:59:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 02:13:02 +0200 |
wenzelm |
* HOL/record:
|
file |
diff |
annotate
|
| Wed, 24 Oct 2001 17:37:58 +0200 |
wenzelm |
* clasimp: ``iff'' declarations now handle conditional rules as well;
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 19:12:37 +0200 |
wenzelm |
* Pure: removed obsolete 'exported' attribute;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2001 19:44:25 +0200 |
wenzelm |
* proper spacing of consecutive markup elements, especially text
|
file |
diff |
annotate
|
| Sat, 20 Oct 2001 20:14:16 +0200 |
wenzelm |
* greatly simplified document preparation setup, including more
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 18:50:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 22:59:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|