src/HOL/Library/Old_Recdef.thy
23 months ago wenzelm 2017-11-26 more symbols;
2015-06-19 wenzelm 2015-06-19 discontinued unused 'defer_recdef';
2015-06-19 wenzelm 2015-06-19 moved sources;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-04 hoelzl 2014-09-04 cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-03-15 wenzelm 2012-03-15 basic support for outer syntax keywords in theory header;
2011-08-02 krauss 2011-08-02 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy