src/HOL/Nominal/nominal_package.ML
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-05 berghofe 2007-04-05 Replaced add_inductive_i by add_inductive_global.
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-03-28 berghofe 2007-03-28 Renamed induct(s)_weak to weak_induct(s) in order to unify naming scheme with the one used in nominal_inductive.
2007-03-27 berghofe 2007-03-27 Exported perm_of_pair, mk_not_sym, and perm_simproc.
2007-03-10 berghofe 2007-03-10 - Changed format of descriptor contained in nominal_datatype_info - Equivariance proof for graph of primrec combinator no longer uses large simpset (more robust).
2007-02-13 berghofe 2007-02-13 Curried and exported mk_perm.
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.
2007-02-06 urbanc 2007-02-06 moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions
2007-02-02 urbanc 2007-02-02 added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-11-27 berghofe 2006-11-27 Additional information about nominal datatypes (descriptor, recursion equations etc.) is now stored in theory.
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-11-15 urbanc 2006-11-15 replaced exists_fresh lemma with a version formulated with obtains; old lemma is available as exists_fresh' (still needed in apply-scripts)
2006-11-14 wenzelm 2006-11-14 InductivePackage.add_inductive_i: canonical argument order;
2006-11-10 wenzelm 2006-11-10 simplified LocalTheory.exit;
2006-10-23 berghofe 2006-10-23 Added freshness context to FCBs.
2006-10-20 berghofe 2006-10-20 Proof of "bs # fK bs us vs" no longer depends on FCBs.
2006-10-19 berghofe 2006-10-19 Induction rule for graph of recursion combinator is now hidden to prevent name collisions with induction rule for nominal datatype.
2006-10-19 berghofe 2006-10-19 Split up FCBs into separate formulae for each binder.
2006-10-13 berghofe 2006-10-13 Adapted to new inductive definition package.
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-06 haftmann 2006-09-06 TypedefPackage.add_typedef_* now yields name of introduced type constructor
2006-08-24 berghofe 2006-08-24 Added premises concerning finite support of recursion results to FCBs.
2006-08-18 berghofe 2006-08-18 - Fixed bug that caused uniqueness proof for recursion combinator to fail for mutually recursive datatypes - Implemented proofs of characteristic equations for recursion combinator.
2006-08-14 berghofe 2006-08-14 Finished implementation of uniqueness proof for recursion combinator.
2006-07-31 berghofe 2006-07-31 Additional freshness constraints for FCB.
2006-07-21 haftmann 2006-07-21 adaption to argument change in primrec_package
2006-07-18 berghofe 2006-07-18 Started implementing uniqueness proof for recursion combinator (still unfinished).
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-07-04 berghofe 2006-07-04 Implemented proofs of equivariance and finite support for graph of recursion combinator.
2006-06-13 wenzelm 2006-06-13 ProjectRule now context dependent;
2006-06-12 berghofe 2006-06-12 Completely rewrote code for defining graph of recursion combinator.
2006-06-09 berghofe 2006-06-09 - Changed naming scheme: names of "internal" constructors now have "_Rep" as suffix - no need to set unique_names to false any longer - Cleaned up a bit (removed occurrences of strip_option and replace_types')
2006-05-24 berghofe 2006-05-24 Extended strong induction rule with additional freshness constraints.
2006-05-16 wenzelm 2006-05-16 Sign.certify_sort;
2006-05-13 wenzelm 2006-05-13 unchecked definitions;
2006-04-28 berghofe 2006-04-28 Renamed "nominal" theory to "Nominal".
2006-04-27 berghofe 2006-04-27 SplitAt -> chop
2006-04-10 berghofe 2006-04-10 Adapted to changed type of add_typedef_i.
2006-03-23 berghofe 2006-03-23 Replaced iteration combinator by recursion combinator.
2006-03-15 berghofe 2006-03-15 add_inst_arity_i renamed to prove_arity.
2006-03-13 berghofe 2006-03-13 First version of function for defining graph of iteration combinator.
2006-02-24 berghofe 2006-02-24 Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-24 berghofe 2006-02-24 Adapted to Florian's recent changes to the AxClass package.
2006-01-23 krauss 2006-01-23 Updated to Isabelle 2006-01-23
2006-01-19 berghofe 2006-01-19 Use generic Simplifier.simp_add attribute instead of Simplifier.simp_add_global.
2006-01-11 berghofe 2006-01-11 Implemented proof of (strong) induction rule.
2006-01-05 wenzelm 2006-01-05 provide projections of induct_weak, induct_unsafe;
2006-01-05 urbanc 2006-01-05 changed the name of the type "nOption" to "noption".
2005-12-10 urbanc 2005-12-10 changed the types in accordance with Florian's changes
2005-12-08 berghofe 2005-12-08 Adapted to new type of PureThy.add_defs_i.
2005-12-05 berghofe 2005-12-05 Adapted to new type of store_thmss(_atts).
2005-11-30 berghofe 2005-11-30 Changed order of predicate arguments and quantifiers in strong induction rule.
2005-11-29 berghofe 2005-11-29 Corrected atom class constraints in strong induction rule.
2005-11-26 berghofe 2005-11-26 Corrected treatment of non-recursive abstraction types.