Nominal-General/nominal_thmdecls.ML
2010-05-27 Christian Urban fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
2010-05-13 Christian Urban removed internal functions from the signature (they are not needed anymore)
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-18 Christian Urban tuned; transformation functions now take a context, a thm and return a thm
2010-04-14 Christian Urban temporary fix for CoreHaskell
2010-04-14 Christian Urban thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
2010-04-14 Christian Urban tuned and removed dead code
2010-04-14 Christian Urban moved a couple of more functions to the library
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-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