src/HOL/Nominal/nominal_package.ML
2008-05-23 haftmann 2008-05-23 moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
2008-05-22 urbanc 2008-05-22 made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-16 berghofe 2008-04-16 Auxiliary permutation functions are no longer declared using add_consts_i, because add_primrec_overloaded can do this as well.
2008-04-16 berghofe 2008-04-16 Adapted to new primrec package.
2008-04-15 wenzelm 2008-04-15 PureThy.hide_fact;
2008-04-15 wenzelm 2008-04-15 overloading perm: use big_name; avoid rebinding of perm_closed -- leftover debug code;
2008-04-14 wenzelm 2008-04-14 overloading of perm: adhoc name prevents duplicate fact names;
2008-04-03 berghofe 2008-04-03 Added skip_mono flag to inductive definition package.
2008-03-29 wenzelm 2008-03-29 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
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.