src/HOL/Nominal/Nominal.thy
2006-01-05 urbanc 2006-01-05 changed the name of the type "nOption" to "noption".
2006-01-04 urbanc 2006-01-04 added "fresh_singleton" lemma
2005-12-22 berghofe 2005-12-22 Tuned syntax for perm.
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-05 urbanc 2005-12-05 ISAR-fied two proofs
2005-11-30 urbanc 2005-11-30 changed \<sim> of permutation equality to \<triangleq> (Jesper wanted to use \<sim>).
2005-11-30 wenzelm 2005-11-30 fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
2005-11-28 urbanc 2005-11-28 ISAR-fied two proofs about equality for abstraction functions.
2005-11-27 urbanc 2005-11-27 added the version of nominal.thy that contains all properties about support of finite sets
2005-11-25 urbanc 2005-11-25 added fsub.thy (poplmark challenge) to the examples directory.
2005-11-14 urbanc 2005-11-14 added a few equivariance lemmas (they need to be automated eventually)
2005-11-02 berghofe 2005-11-02 Moved atom stuff to new file nominal_atoms.ML
2005-11-01 urbanc 2005-11-01 some minor tweaks in some proofs (nothing extraordinary)
2005-10-30 urbanc 2005-10-30 tuned my last commit
2005-10-30 urbanc 2005-10-30 simplified the abs_supp_approx proof and tuned some comments in nominal_permeq.ML
2005-10-28 urbanc 2005-10-28 Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.
2005-10-17 urbanc 2005-10-17 deleted leading space in the definition of fresh
2005-10-17 berghofe 2005-10-17 Initial revision.