2009-10-30 Christian Urban added fv-function
2009-10-30 Cezary Kaliszyk The proper real_alpha
2009-10-30 Cezary Kaliszyk Finding applications and duplicates filtered out in abstractions
2009-10-30 Cezary Kaliszyk Cleaning also in Lam
2009-10-30 Cezary Kaliszyk Cleaning of the interface to lift.
2009-10-29 Cezary Kaliszyk Tried manually lifting real_alpha
2009-10-29 Cezary Kaliszyk More tests in Lam
2009-10-29 Cezary Kaliszyk Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
2009-10-29 Cezary Kaliszyk Using subst for identity definition.
2009-10-29 Cezary Kaliszyk Lifting of the 3 lemmas in LamEx
2009-10-29 Cezary Kaliszyk Fixed wrong CARD definition and removed the "Does not work anymore" comment.
2009-10-29 Christian Urban merged
2009-10-28 Christian Urban updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
2009-10-28 Christian Urban ported all constant definitions to new scheme
2009-10-28 Christian Urban fixed the definition of alpha; this *breaks* some of the experiments
2009-10-28 Cezary Kaliszyk disambiguate ===> syntax
2009-10-28 Cezary Kaliszyk More cleaning in Lam code
2009-10-28 Cezary Kaliszyk cleaned FSet
2009-10-28 Cezary Kaliszyk Some cleaning
2009-10-28 Cezary Kaliszyk Cleaning the unnecessary theorems in 'IntEx'.
2009-10-28 Cezary Kaliszyk Fix also in the general procedure.
2009-10-28 Cezary Kaliszyk merge
2009-10-28 Cezary Kaliszyk Fixes
2009-10-28 Christian Urban updated all definitions
2009-10-28 Christian Urban merged
2009-10-28 Christian Urban added infrastructure for defining lifted constants
2009-10-28 Cezary Kaliszyk First experiments with Lambda
2009-10-28 Cezary Kaliszyk Fixed mistake in const generation, will postpone this.
2009-10-28 Cezary Kaliszyk More finshed proofs and cleaning
2009-10-28 Cezary Kaliszyk Proof of append_rsp
2009-10-28 Christian Urban merged
2009-10-28 Christian Urban added a function for matching types
2009-10-27 Cezary Kaliszyk Manual conversion of equality to equivalence allows lifting append_assoc.
2009-10-27 Cezary Kaliszyk Simplfied interface to repabs_injection.
2009-10-27 Cezary Kaliszyk map_append lifted automatically.
2009-10-27 Cezary Kaliszyk Manually lifted Map_Append.
2009-10-27 Cezary Kaliszyk Merged
2009-10-27 Cezary Kaliszyk Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
2009-10-27 Christian Urban tuned
2009-10-27 Christian Urban merged
2009-10-27 Christian Urban added equiv-thm to the quot_info
2009-10-27 Cezary Kaliszyk Simplifying FSet with new functions.
2009-10-27 Christian Urban added an example about lambda-terms
2009-10-27 Christian Urban made quotients compatiple with Nominal; updated keyword file
2009-10-27 Christian Urban merged
2009-10-27 Cezary Kaliszyk Completely cleaned Int.
2009-10-27 Cezary Kaliszyk Further reordering in Int code.
2009-10-26 Cezary Kaliszyk Simplifying Int.
2009-10-26 Cezary Kaliszyk Merge
2009-10-26 Cezary Kaliszyk Simplifying Int and Working on map
2009-10-26 Christian Urban merged
2009-10-26 Cezary Kaliszyk Simplifying code in int
2009-10-26 Cezary Kaliszyk Symmetry of integer addition
2009-10-26 Cezary Kaliszyk Finished the code for adding lower defs, and more things moved to QuotMain
2009-10-26 Cezary Kaliszyk Making all the definitions from the original ones
2009-10-26 Cezary Kaliszyk Finished COND_PRS proof.
2009-10-26 Cezary Kaliszyk Cleaning and fixing.
2009-10-26 Christian Urban updated with quotient_def
2009-10-25 Christian Urban added code for declaring map-functions
2009-10-24 Christian Urban added "print_quotients" command to th ekeyword file
(0) -100 -60 +60 +100 +300 +1000 +3000 tip