Nominal/Ex/Lambda.thy
2010-04-16 Christian Urban automatic proofs for equivariance of alphas
2010-04-16 Cezary Kaliszyk Finished proof in Lambda.thy
2010-04-16 Christian Urban attempt to manual prove eqvt for alpha
2010-04-16 Christian Urban some tuning of eqvt-infrastructure
2010-04-14 Christian Urban deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
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 first working version of the automatic equivariance procedure
2010-04-14 Christian Urban preliminary tests
2010-04-13 Christian Urban made everything to compile
2010-04-12 Christian Urban some small tunings (incompleted work in Lambda.thy)
2010-04-12 Christian Urban early ott paper
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 a few tests
2010-04-09 Christian Urban changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
2010-04-09 Christian Urban renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
less more (0) tip