FSet.thy
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 Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
2009-10-27 Cezary Kaliszyk Simplifying FSet with new functions.
2009-10-26 Cezary Kaliszyk Simplifying Int and Working on map
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 Cleaning and fixing.
2009-10-24 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall)
2009-10-24 Christian Urban changed the definitions of liftet constants to use fun_maps
2009-10-24 Cezary Kaliszyk Finally lifted induction, with some manually added simplification lemmas.
2009-10-24 cek Merge
2009-10-24 Cezary Kaliszyk Preparing infrastructire for LAMBDA_PRS
less more (0) -15 tip