Nominal/nominal_dt_supp.ML
2010-12-06 Christian Urban automated alpha_perm_bn theorems
2010-12-06 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-11-15 Christian Urban proved that bn functions return a finite set
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-09-27 Christian Urban added postprocessed fresh-lemmas for constructors
2010-09-27 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality
2010-09-27 Christian Urban more consistent naming in Abs.thy
2010-09-22 Christian Urban removed dead code
2010-09-22 Christian Urban made supp proofs more robust by not using the standard induction; renamed some example files
2010-09-10 Christian Urban supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
2010-08-28 Christian Urban added fs-instance proofs
2010-08-28 Christian Urban added proofs for fsupp properties
2010-08-28 Christian Urban fiexed problem with constructors that have no arguments
2010-08-28 Christian Urban proved supports lemmas
less more (0) tip