Nominal-General/nominal_permeq.ML
2010-05-21 Cezary Kaliszyk Renamings
2010-05-17 Christian Urban updated to new Isabelle (More_Conv -> Conv)
2010-05-13 Christian Urban properly declared outer keyword
2010-05-09 Christian Urban added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
2010-05-06 Cezary Kaliszyk Fixes for new isabelle
2010-05-05 Christian Urban solved the problem with equivariance by first eta-normalising the goal
2010-04-25 Christian Urban tuned and cleaned
2010-04-16 Christian Urban automatic proofs for equivariance of alphas
2010-04-14 Christian Urban moved a couple of more functions to the library
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