2011-06-09 Cezary Kaliszyk Minor simplification
2011-06-09 Cezary Kaliszyk abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
2011-06-09 Cezary Kaliszyk More experiments with 'default'
2011-06-08 Cezary Kaliszyk Finished the proof with the invariant
2011-06-08 Cezary Kaliszyk Issue with 'default'
2011-06-08 Christian Urban merged
2011-06-08 Christian Urban merged
2011-06-08 Christian Urban using the option "default" the function package allows one to give an explicit default value
2011-06-08 Cezary Kaliszyk Simpler proof of TypeSchemes/substs
2011-06-08 Cezary Kaliszyk Simplify fcb_res
2011-06-08 Cezary Kaliszyk FCB for res binding and simplified proof of subst for type schemes
2011-06-07 Cezary Kaliszyk Simplify ln-trans proof
2011-06-07 Cezary Kaliszyk cbvs can be easily defined without an invariant
2011-06-07 Christian Urban defined the "count-bound-variables-occurences" function which has an accumulator like trans
2011-06-07 Christian Urban merged
2011-06-07 Cezary Kaliszyk remove garbage (proofs that assumes the invariant outside function)
2011-06-07 Cezary Kaliszyk Proof of trans with invariant
2011-06-07 Cezary Kaliszyk Testing invariant in Lambda_F_T
2011-06-07 Christian Urban cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
2011-06-07 Christian Urban fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
2011-06-06 Christian Urban slightly stronger property in fundef_ex_prop
2011-06-05 Christian Urban added an option for an invariant (at the moment only a stub)
2011-06-05 Christian Urban added a more general lemma fro fundef_ex1
2011-06-04 Cezary Kaliszyk Trying the induction on the graph
2011-06-04 Cezary Kaliszyk Finish and test the locale approach
2011-06-03 Cezary Kaliszyk FiniteSupp precondition in the function is enough to get rid of completeness obligationss
2011-06-03 Christian Urban recursion combinator inside a locale
2011-06-03 Cezary Kaliszyk merge
2011-06-03 Cezary Kaliszyk F for lambda used to define translation to locally nameless
2011-06-02 Christian Urban typo
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 tip