src/HOL/Nominal/nominal_package.ML
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.
2005-10-17 berghofe 2005-10-17 Improved proof of injectivity theorems to make it work on "ordinary" function types as well.
2005-10-17 berghofe 2005-10-17 Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17 berghofe 2005-10-17 Implemented proofs for support and freshness theorems.
2005-10-17 berghofe 2005-10-17 Initial revision.