src/HOL/Nominal/nominal_package.ML
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-02-25 wenzelm 2008-02-25 inductive package: simplified group handling;
2008-02-14 berghofe 2008-02-14 Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.
2008-01-28 berghofe 2008-01-28 Tuned uniqueness proof for recursion combinator.
2008-01-26 wenzelm 2008-01-26 avoid redundant escaping of Isabelle symbols;
2008-01-26 wenzelm 2008-01-26 internal inductive: fresh theorem group;
2008-01-24 berghofe 2008-01-24 Reimplemented proof of strong induction theorem.
2008-01-03 berghofe 2008-01-03 Added function fresh_const.
2007-12-17 berghofe 2007-12-17 Deleted copy of indtac.
2007-12-06 haftmann 2007-12-06 added new primrec package
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-02 wenzelm 2007-10-02 inductive: mark internal theorems as Thm.internalK;
2007-09-28 berghofe 2007-09-28 Adapted to changes in interface of add_inductive_i.
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-08-28 berghofe 2007-08-28 Got rid of large simpset in proof of characteristic equations for freshness.
2007-08-10 haftmann 2007-08-10 ClassPackage renamed to Class
2007-08-01 wenzelm 2007-08-01 tuned config options: eliminated separate attribute "option";
2007-07-31 wenzelm 2007-07-31 replaced dtK ref by datatype_distinctness_limit configuration option;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-05-19 haftmann 2007-05-19 constant op @ now named append
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')