src/HOL/Tools/primrec_package.ML
2009-05-18 haftmann 2009-05-18 introduced Thm.generatedK
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-05-16 bulwahn 2009-05-16 added collection of simplification rules of recursive functions for quickcheck
2009-03-12 wenzelm 2009-03-12 simplified preparation and outer parsing of specification; export extern cmd interfaces as well;
2009-03-11 wenzelm 2009-03-11 merged
2009-03-11 haftmann 2009-03-11 corrected type inference of primitive definitions
2009-03-11 wenzelm 2009-03-11 explicit Binding.qualified_name -- prevents implicitly qualified bstring;
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-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
2009-02-09 blanchet 2009-02-09 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.
2009-02-06 blanchet 2009-02-06 Merged.
2009-02-06 blanchet 2009-02-06 Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.
2009-02-05 haftmann 2009-02-05 code attribute applied before user attributes
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-12-31 wenzelm 2008-12-31 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-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-10-07 haftmann 2008-10-07 proper default codegen attribute
2008-09-29 wenzelm 2008-09-29 LocalTheory.exit_global;
2008-09-03 wenzelm 2008-09-03 Name.qualified;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-06-20 haftmann 2008-06-20 fixed bind error for malformed primrec specifications
2008-04-16 berghofe 2008-04-16 Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
2008-04-04 haftmann 2008-04-04 prefix for equations in primrec specifications
2008-02-25 wenzelm 2008-02-25 LocalTheory.set_group for user command;
2007-12-11 haftmann 2007-12-11 dropped induction rule
2007-12-07 haftmann 2007-12-07 proper treatment of code theorems for primrec
2007-12-07 haftmann 2007-12-07 tuned further
2007-12-06 haftmann 2007-12-06 fixed slip
2007-12-06 haftmann 2007-12-06 authentic primrec
2007-12-06 haftmann 2007-12-06 added new primrec package
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-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-08-30 wenzelm 2007-08-30 replaced ProofContext.infer_types by general Syntax.check_terms;
2007-07-11 berghofe 2007-07-11 Function unify_consts moved from OldInductivePackage to PrimrecPackage.
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