Nominal-General/nominal_library.ML
2010-11-12 Christian Urban automated permute_bn functions (raw ones first)
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-11-07 Christian Urban fixed locally the problem with the function package; all tests work again
2010-09-20 Christian Urban introduced a general procedure for structural inductions; simplified reflexivity proof
2010-09-12 Christian Urban tuned code
2010-09-10 Christian Urban supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
2010-09-03 Christian Urban made the fv-definition aggree more with alpha (needed in the support proofs)
2010-08-28 Christian Urban added proofs for fsupp properties
2010-08-28 Christian Urban proved supports lemmas
2010-08-28 Christian Urban updated to new Isabelle
2010-08-19 Christian Urban used @{const_name} hopefully everywhere
2010-08-17 Christian Urban improved runtime slightly, by constructing an explicit size measure for the function definitions
2010-08-17 Christian Urban deleted unused code
2010-08-17 Christian Urban improved code
2010-08-15 Christian Urban simplified code
2010-08-14 Christian Urban improved code
2010-08-14 Christian Urban more experiments with lifting
2010-07-31 Christian Urban introduced a general alpha_prove method
2010-07-27 Christian Urban fixed order of fold_union to make alpha and fv agree
2010-07-19 Christian Urban minor polishing
2010-06-09 Christian Urban transitivity proofs done
2010-06-07 Christian Urban work on transitivity proof
2010-05-31 Christian Urban all raw definitions are defined using function
2010-05-24 Christian Urban alpha works now
2010-05-20 Christian Urban moved some mk_union and mk_diff into the library
2010-05-20 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
2010-04-29 Christian Urban added basic functions for constructing supp-terms
2010-04-27 Christian Urban some tuning
2010-04-27 Christian Urban moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
2010-04-20 Christian Urban optimised the code of define_raw_perm
2010-04-19 Christian Urban tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
2010-04-18 Christian Urban moved some general function into nominal_library.ML
2010-04-14 Christian Urban moved a couple of more functions to the library
2010-04-14 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file
less more (0) tip