2010-02-02 Cezary Kaliszyk First experiments in Terms.
2010-02-02 Cezary Kaliszyk LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
2010-02-02 Cezary Kaliszyk Disambiguating the syntax.
2010-02-02 Cezary Kaliszyk Minor uncommited changes from LamEx2.
2010-02-02 Cezary Kaliszyk Some equivariance machinery that comes useful in LF.
2010-02-02 Cezary Kaliszyk Generalized the eqvt proof for single binders.
2010-02-02 Cezary Kaliszyk With induct instead of induct_tac, just one induction is sufficient.
2010-02-02 Cezary Kaliszyk General alpha_gen_trans for one-variable abstraction.
2010-02-02 Cezary Kaliszyk With unfolding Rep/Abs_eqvt no longer needed.
2010-02-02 Cezary Kaliszyk Lam2 finished apart from Rep_eqvt.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk All should be ok now.
2010-02-01 Christian Urban repaired according to changes in Abs.thy
2010-02-01 Christian Urban added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
2010-02-01 Christian Urban cleaned
2010-02-01 Christian Urban updated from huffman
2010-02-01 Christian Urban updated from nominal-huffman
2010-02-01 Cezary Kaliszyk Fixed wrong rename.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk Lambda based on alpha_gen, under construction.
2010-02-01 Christian Urban updated from huffman - repo
2010-02-01 Christian Urban renamed Abst/abst to Abs/abs
2010-02-01 Christian Urban got rid of RAbst type - is now just pairs
2010-02-01 Cezary Kaliszyk Monotonicity of ~~gen, needed for using it in inductive definitions.
2010-02-01 Cezary Kaliszyk The current state of fv vs supp proofs in LF.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk More proofs in the LF example.
2010-02-01 Christian Urban merged
2010-02-01 Christian Urban slight tuning
2010-02-01 Christian Urban renamed function according to the name of the constant
2010-02-01 Christian Urban fixed problem with Bex1_rel renaming
2010-02-01 Cezary Kaliszyk Ported LF to the generic lambda and solved the simpler _supp cases.
2010-01-30 Christian Urban merged
2010-01-30 Christian Urban introduced a generic alpha (but not sure whether it is helpful)
2010-01-29 Cezary Kaliszyk More in the LF example in the new nominal way, all is clear until support.
2010-01-29 Cezary Kaliszyk Fixed the induction problem + some more proofs.
2010-01-29 Cezary Kaliszyk equivariance of rfv and alpha.
2010-01-29 Cezary Kaliszyk Added the experiments with fun and function.
2010-01-29 Christian Urban now also final step is proved - the supp of lambdas is now completely characterised
2010-01-28 Christian Urban the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
2010-01-28 Christian Urban improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban general abstraction operator and complete characterisation of its support and freshness
2010-01-28 Cezary Kaliszyk Ported existing part of LF to new permutations and alphas.
2010-01-28 Christian Urban attempt of a general abstraction operator
2010-01-28 Christian Urban attempt to prove equivalence between alpha definitions
2010-01-28 Cezary Kaliszyk End of renaming.
2010-01-28 Cezary Kaliszyk Minor when looking at lam.distinct and lam.inject
2010-01-28 Cezary Kaliszyk Renamed Bexeq to Bex1_rel
2010-01-28 Cezary Kaliszyk Substracting bounds from free variables.
2010-01-28 Cezary Kaliszyk Improper interface for datatype and function packages and proper interface lateron.
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban minor
2010-01-28 Christian Urban test about supp/freshness for lam (old proofs work in principle - for single binders)
2010-01-28 Cezary Kaliszyk Recommited the changes for nitpick
2010-01-27 Cezary Kaliszyk Correct types which fixes the printing.
2010-01-27 Cezary Kaliszyk fv for subterms
2010-01-27 Cezary Kaliszyk Fix the problem with later examples. Maybe need to go back to textual specifications.
2010-01-27 Cezary Kaliszyk Some processing of variables in constructors to get free variables.
2010-01-27 Cezary Kaliszyk Parsing of the input as terms and types, and passing them as such to the function package.
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip