src/HOL/Nominal/nominal_atoms.ML
2006-01-05 urbanc 2006-01-05 changed the name of the type "nOption" to "noption".
2005-12-19 urbanc 2005-12-19 made the changes according to Florian's re-arranging of tuples (everything up to 19th December).
2005-12-19 urbanc 2005-12-19 added proofs to show that every atom-kind combination is in the respective finite-support class (now have to adjust the files according to Florian's changes)
2005-12-19 urbanc 2005-12-19 added thms to perm_compose (so far only composition theorems were included where the type of the permutation was equal)
2005-12-19 urbanc 2005-12-19 tuned one comment
2005-12-18 urbanc 2005-12-18 more cleaning up - this time of the cp-instance proofs
2005-12-18 urbanc 2005-12-18 improved the finite-support proof added finite support proof for options (I am surprised that one does not need more fs-proofs; at the moment only lists, products, units and atoms are shown to be finitely supported (of course also every nominal datatype is finitely supported)) deleted pt_bool_inst - not necessary because discrete types are treated separately in nominal_atoms
2005-12-18 urbanc 2005-12-18 improved the code for showing that a type is in the pt-axclass (I try to slowly overcome my incompetence with such ML-code).
2005-12-16 urbanc 2005-12-16 added container-lemma fresh_eqvt (definition: container-lemma contains all instantiations of a lemma from the general theory)
2005-12-13 urbanc 2005-12-13 added a fresh_left lemma that contains all instantiation for the various atom-types.
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 urbanc 2005-12-05 added code to say that discrete types (nat, bool, char) are instances of cp_*_*.
2005-11-30 urbanc 2005-11-30 added facilities to prove the pt and fs instances for discrete types
2005-11-29 urbanc 2005-11-29 made some of the theorem look-ups static (by using thm instead of PureThy.get_thm)
2005-11-27 urbanc 2005-11-27 finished cleaning up the parts that collect lemmas (with instantiations) under some general names
2005-11-07 urbanc 2005-11-07 used the function Library.product for the cprod from Stefan
2005-11-02 berghofe 2005-11-02 Moved atom stuff to new file nominal_atoms.ML