src/HOL/Quotient_Examples/FSet.thy
Tue, 19 Oct 2010 15:13:35 +0100 Christian Urban tuned
Mon, 18 Oct 2010 14:25:15 +0100 Christian Urban reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
Fri, 15 Oct 2010 21:50:26 +0900 Cezary Kaliszyk FSet: definition changes propagated from Nominal and more use of 'descending' tactic
Fri, 15 Oct 2010 21:47:45 +0900 Cezary Kaliszyk FSet tuned
Fri, 15 Oct 2010 21:46:45 +0900 Cezary Kaliszyk FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Tue, 29 Jun 2010 17:03:59 +0100 Christian Urban cleaned by using descending instead of lifting
less more (0) -10 -8 tip