src/HOL/Fun_Def.thy
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized module name and setup;
2014-05-04 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-04-23 blanchet 2014-04-23 move size hooks together, with new one preceding old one and sharing same theory data
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-07 blanchet 2014-03-07 tuning
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain