src/HOL/Nominal/nominal_package.ML
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.
2005-11-25 urbanc 2005-11-25 added fsub.thy (poplmark challenge) to the examples directory.
2005-11-25 berghofe 2005-11-25 Fixed problem with strong induction theorem for datatypes containing no atom types (ind_sort was the empty sort in this case).
2005-11-10 urbanc 2005-11-10 called the induction principle "unsafe" instead of "test".
2005-11-07 berghofe 2005-11-07 Added strong induction theorem (currently only axiomatized!).
2005-11-07 urbanc 2005-11-07 added thms perm, distinct and fresh to the simplifier. One would liket to add also inject, but this causes problems with "congruences" like Lam [a].t1 = Lam [b].t2 P (Lam [a].t1) ----------------------- P (Lam [b].t2) because the equation "Lam [a].t1 = Lam [b].t2" would simplify to "[a].t1 = [b].t2" and then the goal is not true just by simplification.
2005-11-02 berghofe 2005-11-02 Moved atom stuff to new file nominal_atoms.ML
2005-11-02 urbanc 2005-11-02 - completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names
2005-11-02 berghofe 2005-11-02 Added code for proving that new datatype has finite support.
2005-11-02 urbanc 2005-11-02 added the collection of lemmas "supp_at"
2005-10-29 urbanc 2005-10-29 1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")
2005-10-28 urbanc 2005-10-28 fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"
2005-10-28 berghofe 2005-10-28 Implemented proof of weak induction theorem.
2005-10-28 berghofe 2005-10-28 Removed legacy prove_goalw_cterm command.