| 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
|