isabelle: Changelog

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54622

repaired inconsistency introduced in transiting to 'Local_Theory.define'

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54621

docs for forgotten BNF theorems

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54620

tuning

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54619

added 'cong' attribute to 'map_cong'

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54618

avoid user-level 'Specification.definition' for internal constructions (to avoid e.g. automatic code generation behavior)

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54617

don't try to register code equations in a locale with assumptions

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54616

minor doc update

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54615

generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)

blanchet [Mon, 02 Dec 2013 20:31:54 +0100] rev 54614

simpler code

panny [Sun, 01 Dec 2013 19:32:57 +0100] rev 54613

more work towards "exhaustive"

isabelle