src/ZF/Tools/primrec_package.ML
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-05-11 wenzelm 2013-05-11 prefer explicitly qualified exceptions, which is particular important for robust handlers;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-18 haftmann 2010-08-18 deglobalization
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-16 wenzelm 2010-05-16 prefer structure Parse_Spec;
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
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-01-21 haftmann 2009-01-21 binding replaces bstring
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-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
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-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-08-05 wenzelm 2006-08-05 tuned;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-02-07 wenzelm 2006-02-07 has_duplicates;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2001-11-15 wenzelm 2001-11-15 avoid handle _;
2001-11-14 wenzelm 2001-11-14 fix path prefix;
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-06-28 paulson 2000-06-28 no longer depends upon a prior "open Ind_Syntax" from elsewhere
2000-05-05 wenzelm 2000-05-05 use Sign.simple_read_term;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;