FSet.thy
Mon, 26 Oct 2009 15:31:53 +0100 Cezary Kaliszyk Simplifying Int and Working on map
Mon, 26 Oct 2009 11:55:36 +0100 Cezary Kaliszyk Finished the code for adding lower defs, and more things moved to QuotMain
Mon, 26 Oct 2009 11:34:02 +0100 Cezary Kaliszyk Making all the definitions from the original ones
Mon, 26 Oct 2009 10:02:50 +0100 Cezary Kaliszyk Cleaning and fixing.
Sun, 25 Oct 2009 01:15:03 +0200 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall)
Sat, 24 Oct 2009 18:17:38 +0200 Christian Urban changed the definitions of liftet constants to use fun_maps
Sat, 24 Oct 2009 17:29:27 +0200 Cezary Kaliszyk Finally lifted induction, with some manually added simplification lemmas.
Sat, 24 Oct 2009 16:15:33 +0200 cek Merge
less more (0) -10 -8 tip