FSet.thy
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
less more (0) -14 tip