Nominal-General/Nominal2_Eqvt.thy
2010-05-02 Christian Urban removed duplicate eqvt attribute
2010-04-30 Christian Urban added eqvt-lemmas for Bex, Ball and Union
2010-04-30 Christian Urban reorganised eqvt-file (now uses perm_simp already)
2010-04-28 Christian Urban simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
2010-04-27 Christian Urban moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
2010-04-26 Christian Urban rewrote eqvts_raw to be a symtab, that can be looked up
2010-04-25 Christian Urban tuned and cleaned
2010-04-22 Christian Urban tuned parser
2010-04-22 Christian Urban moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
2010-04-18 Christian Urban tuned
2010-04-18 Christian Urban tuned
2010-04-18 Christian Urban preliminary parser for perm_simp metod
2010-04-16 Christian Urban automatic proofs for equivariance of alphas
2010-04-14 Christian Urban tuned and removed dead code
2010-04-14 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file
2010-04-14 Christian Urban deleted test
2010-04-12 Christian Urban moved equivariance of map into Nominal2_Eqvt file
2010-04-12 Christian Urban implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
2010-04-11 Christian Urban fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
2010-04-11 Christian Urban used warning instead of tracing (does not seem to produce stable output)
2010-04-11 Christian Urban added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
2010-04-09 Christian Urban changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
2010-04-04 Christian Urban separated general nominal theory into separate folder
less more (0) tip