src/HOL/Nominal/nominal_inductive2.ML
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm 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;
Thu, 26 Feb 2009 16:34:03 +0100 berghofe Added postprocessing rules for fresh_star.
Wed, 25 Feb 2009 11:05:06 +0100 berghofe nominal_inductive and equivariance now work on local_theory.
Wed, 21 Jan 2009 18:27:43 +0100 haftmann binding replaces bstring
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm eliminated OldTerm.(add_)term_consts;
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 10 Nov 2008 17:37:25 +0100 berghofe Streamlined functions for accessing information about atoms.
Tue, 21 Oct 2008 21:20:17 +0200 berghofe More general, still experimental version of nominal_inductive for
less more (0) tip