src/HOL/Tools/old_primrec_package.ML
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-10 blanchet 2009-02-10 Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-01 wenzelm 2009-01-01 Term.add_consts;
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-09-22 haftmann 2008-09-22 fixed headers
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (not really needed);
2007-12-06 haftmann 2007-12-06 -authentic primrec
2007-12-06 haftmann 2007-12-06 added new primrec package