QuotMain.thy
2009-10-26 Cezary Kaliszyk Cleaning and fixing.
2009-10-25 Christian Urban added code for declaring map-functions
2009-10-24 Christian Urban added data-storage about the quotients
2009-10-24 Christian Urban changed the definitions of liftet constants to use fun_maps
2009-10-24 Christian Urban moved the map_funs setup into QuotMain
2009-10-24 cek Undid wrong merge
2009-10-24 cek Cleaning the mess
2009-10-23 Christian Urban fixed problem with incorrect ABS/REP name
2009-10-23 Cezary Kaliszyk Split Finite Set example into separate file
2009-10-23 Cezary Kaliszyk eqsubst_tac
2009-10-23 Cezary Kaliszyk Trying to get a simpler lemma with the whole infrastructure
2009-10-23 Cezary Kaliszyk Using RANGE tactical allows getting rid of the quotients immediately.
2009-10-22 Cezary Kaliszyk Further developing the tactic and simplifying the proof
2009-10-22 Cezary Kaliszyk res_forall_rsp_tac further simplifies the proof
less more (0) -100 -14 tip