FSet.thy
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
2009-10-24 Christian Urban moved the map_funs setup into QuotMain
2009-10-24 Cezary Kaliszyk Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
2009-10-24 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
2009-10-24 cek Cleaning the mess
2009-10-24 cek Merge
2009-10-24 cek Better tactic and simplified the proof further
2009-10-23 Christian Urban fixed problem with incorrect ABS/REP name
2009-10-23 Cezary Kaliszyk Stronger tactic, simpler proof.
2009-10-23 Cezary Kaliszyk Split Finite Set example into separate file
less more (0) tip