src/HOL/Nominal/nominal_inductive2.ML
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-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-11 haftmann 2009-03-11 HOLogic.mk_set, HOLogic.dest_set
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-06 haftmann 2009-03-06 merged
2009-03-06 haftmann 2009-03-06 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05 haftmann 2009-03-05 merged
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
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-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
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-26 berghofe 2009-02-26 Added postprocessing rules for fresh_star.
2009-02-25 berghofe 2009-02-25 nominal_inductive and equivariance now work on local_theory.
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-01 wenzelm 2009-01-01 eliminated OldTerm.(add_)term_consts;
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-10 berghofe 2008-11-10 Streamlined functions for accessing information about atoms.
2008-10-21 berghofe 2008-10-21 More general, still experimental version of nominal_inductive for avoiding sets of names.