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 |