| Thu, 14 Jan 2016 13:51:13 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Jan 2016 12:20:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Jan 2016 12:11:22 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Wed, 13 Jan 2016 23:37:55 +0100 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Wed, 13 Jan 2016 23:25:18 +0100 |
wenzelm |
tuned syntax;
|
changeset |
files
|
| Wed, 13 Jan 2016 23:07:06 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
changeset |
files
|
| Wed, 13 Jan 2016 23:02:28 +0100 |
wenzelm |
eliminated spurious Unicode;
|
changeset |
files
|
| Wed, 13 Jan 2016 21:44:26 +0100 |
wenzelm |
clarified example;
|
changeset |
files
|
| Wed, 13 Jan 2016 21:15:23 +0100 |
wenzelm |
updated section on "Overloaded constant definitions";
|
changeset |
files
|
| Wed, 13 Jan 2016 20:19:49 +0100 |
wenzelm |
more doc content;
|
changeset |
files
|
| Wed, 13 Jan 2016 17:05:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Jan 2016 16:55:56 +0100 |
wenzelm |
removed old 'defs' command;
|
changeset |
files
|
| Wed, 13 Jan 2016 16:41:32 +0100 |
wenzelm |
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
|
changeset |
files
|
| Wed, 13 Jan 2016 16:01:03 +0100 |
wenzelm |
more doc content;
|
changeset |
files
|
| Wed, 13 Jan 2016 15:59:37 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Wed, 13 Jan 2016 15:58:39 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 13 Jan 2016 15:46:21 +0100 |
wenzelm |
proper relative symlink;
|
changeset |
files
|
| Wed, 13 Jan 2016 15:17:11 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Jan 2016 15:09:34 +0100 |
wenzelm |
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
|
changeset |
files
|
| Wed, 13 Jan 2016 09:38:24 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 13 Jan 2016 09:38:16 +0100 |
nipkow |
tuned layout
|
changeset |
files
|
| Wed, 13 Jan 2016 09:09:38 +0100 |
blanchet |
updated NEWS
|
changeset |
files
|
| Wed, 13 Jan 2016 09:09:37 +0100 |
blanchet |
generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
|
changeset |
files
|
| Wed, 13 Jan 2016 00:12:43 +0100 |
wenzelm |
more good NEWS;
|
changeset |
files
|
| Tue, 12 Jan 2016 23:40:33 +0100 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Tue, 12 Jan 2016 20:05:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 12 Jan 2016 19:58:17 +0100 |
wenzelm |
updated old screenshots, added new screenshots;
|
changeset |
files
|
| Tue, 12 Jan 2016 15:43:26 +0100 |
wenzelm |
more explicit errors for control symbols that are left-over after Markdown parsing;
|
changeset |
files
|
| Tue, 12 Jan 2016 14:41:35 +0100 |
wenzelm |
removed in anticipation of c92d82c3f41b -- demolition after renovation;
|
changeset |
files
|
| Tue, 12 Jan 2016 11:49:35 +0100 |
wenzelm |
eliminated old defs;
|
changeset |
files
|