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