src/HOL/Nominal/nominal_inductive.ML
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2011-09-13 haftmann 2011-09-13 tuned
2011-09-10 haftmann 2011-09-10 more modularization
2011-09-03 haftmann 2011-09-03 tuned specifications
2011-08-01 nipkow 2011-08-01 infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-04-27 wenzelm 2010-04-27 really minimize sorts after certification -- looks like this is intended here;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-20 Christian Urban 2009-11-20 use of thm-antiquotation
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-26 wenzelm 2009-07-26 SUBPROOF/Obtain.result: named params;
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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;