src/HOL/Nominal/nominal_inductive.ML
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-03 haftmann 2009-07-03 nominal.ML is nominal_datatype.ML
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
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-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-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-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 eliminated OldTerm.add_term_free_names;
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-08-13 berghofe 2008-08-13 Changed proof of strong induction rule to avoid infinite loop when premises of introduction rules contain equations.
2008-08-04 berghofe 2008-08-04 - corrected bogus comment for function inst_conj_all - tuned function obtain_fresh_name
2008-07-03 berghofe 2008-07-03 Rewrote code to use swap_simps rather than calc_atm (which tends to produce ridiculously large nested if-expressions).
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25 berghofe 2008-06-25 - Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type
2008-06-16 wenzelm 2008-06-16 allE_Nil: only one copy, proven in regular theory source;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-07 wenzelm 2008-04-07 renamed iterated forall_conv to params_conv;
2008-03-20 berghofe 2008-03-20 Equivariance prover now uses permutation simprocs as well.
2008-03-20 haftmann 2008-03-20 more antiquotations
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2008-01-03 berghofe 2008-01-03 Implemented proof of strong case analysis rule.
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 tuned Induct interface: prefer pred'' over set'';
2007-10-04 wenzelm 2007-10-04 Conv.forall_conv: proper context;
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-28 berghofe 2007-09-28 prove_strong_ind now uses InductivePackage.rulify.
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-09-13 berghofe 2007-09-13 Generalized equivariance and nominal_inductive commands to inductive definitions involving arbitrary monotone operators.
2007-07-03 wenzelm 2007-07-03 Conjunction.mk_conjunction_balanced;
2007-05-10 wenzelm 2007-05-10 Thm.first_order_match;
2007-04-25 berghofe 2007-04-25 eqvt_tac now instantiates introduction rules before applying them.
2007-04-20 berghofe 2007-04-20 Modified eqvt_tac to avoid failure due to introduction rules whose premises contain variables that do not occur in the conclusion.
2007-04-19 berghofe 2007-04-19 nominal_inductive no longer proves equivariance.
2007-03-28 berghofe 2007-03-28 - Improved error messages in equivariance proof - Renamed <predicate>_eqvt to <predicate>.eqvt
2007-03-27 berghofe 2007-03-27 Implemented proof of strong induction rule.
2007-02-13 berghofe 2007-02-13 First steps towards strengthening of induction rules for inductively defined predicates involving nominal datatypes.