src/HOL/Fun_Def.thy
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-07 blanchet 2015-07-07 have the installed termination prover take a 'quiet' flag
2015-04-08 wenzelm 2015-04-08 tuned signature;
2014-12-15 blanchet 2014-12-15 renamed theory file
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-29 wenzelm 2014-10-29 modernized setup; tuned whitespace;
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