Nominal/NewAlpha.thy
2010-05-27 Christian Urban merged
2010-05-24 Christian Urban tuned
2010-05-24 Christian Urban alpha works now
2010-05-23 Christian Urban started to work on alpha
2010-05-22 Christian Urban properly exported bn_descr
2010-05-20 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
2010-05-27 Christian Urban fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
2010-05-14 Cezary Kaliszyk Proper fv/alpha for multiple compound binders
2010-05-12 Cezary Kaliszyk Use raw_induct instead of induct
2010-05-10 Cezary Kaliszyk Use mk_compound_fv' and mk_compound_rel'
2010-05-06 Cezary Kaliszyk Fixes for new Isabelle
2010-05-06 Cezary Kaliszyk compound versions with prod_rel and prod_fun, not made default yet.
2010-05-02 Christian Urban replaced make_pair with library function HOLogic.mk_prod
2010-04-30 Cezary Kaliszyk Change signature of fv and alpha generation.
2010-04-29 Cezary Kaliszyk New Alpha.
less more (0) tip