src/HOL/Tools/primrec_package.ML
2007-04-18 wenzelm 2007-04-18 simplified ProofContext.infer_types(_pats);
2007-04-15 wenzelm 2007-04-15 proper ProofContext.infer_types;
2007-03-20 haftmann 2007-03-20 switched exception from arbitrary to undefined
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-10-20 haftmann 2006-10-20 fold cleanup
2006-10-13 berghofe 2006-10-13 Moved old inductive package to old_inductive_package.ML
2006-10-02 haftmann 2006-10-02 added gen_primrec
2006-07-21 haftmann 2006-07-21 exported equation transformator
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-05-20 wenzelm 2006-05-20 added syntax for 'unchecked';
2006-05-13 wenzelm 2006-05-13 added add_primrec_unchecked_i;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to 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;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 removed thms 'swap' and 'nth_map' from ML toplevel
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-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-07-08 berghofe 2005-07-08 Some changes to allow mutually recursive, overloaded functions with same name.
2005-07-01 berghofe 2005-07-01 Adapted to new interface of RecfunCodegen.add.
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.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-21 wenzelm 2004-05-21 tuned message;
2003-11-18 berghofe 2003-11-18 Improved error handling: add_primrec now prints out ill-formed equation in case of parse errors.
2002-10-10 berghofe 2002-10-10 Reimplemented parts of datatype package dealing with datatypes involving function types. Now also supports functions with more than one argument.
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2001-12-12 berghofe 2001-12-12 Improved error messages.
2001-12-10 berghofe 2001-12-10 Recursive equations to be used for code generation are now registered via RecfunCodegen.add
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-14 wenzelm 2001-11-14 store original simps for codegen;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2001-10-18 wenzelm 2001-10-18 GPLed;
2001-08-31 wenzelm 2001-08-31 tuned headers;
2000-11-28 wenzelm 2000-11-28 RuleCases.save;
2000-08-10 berghofe 2000-08-10 Equations that are added to the simpset now have proper names.
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-05-25 paulson 2000-05-25 improved error msgs, listing variable names
2000-03-15 berghofe 2000-03-15 Added new theory data slot for primrec equations.
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.; prepare induct rule (case names);
1999-10-21 wenzelm 1999-10-21 proper handling of axioms / defs;
1999-10-05 berghofe 1999-10-05 Got rid of readtm.
1999-09-20 berghofe 1999-09-20 Fixed bug in add_primrec which caused non-informative error message.
1999-08-02 wenzelm 1999-08-02 tuned outer syntax;
1999-07-16 berghofe 1999-07-16 - Now also supports arbitrarily branching datatypes. - Fixed bug (in some rare cases, recursive constants were inconsistently typed in different primrec equations).
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
1999-04-14 wenzelm 1999-04-14 triple_swap;