| Fri, 15 Oct 2010 21:46:45 +0900 | Cezary Kaliszyk | FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash | file | diff | annotate |
| 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 | file | diff | annotate |
| Tue, 07 Sep 2010 10:05:19 +0200 | nipkow | expand_fun_eq -> ext_iff | file | diff | annotate |
| Tue, 29 Jun 2010 17:03:59 +0100 | Christian Urban | cleaned by using descending instead of lifting | file | diff | annotate |
| Wed, 23 Jun 2010 08:42:41 +0200 | Cezary Kaliszyk | Replace 'list_rel' by 'list_all2'; they are equivalent. | file | diff | annotate |
| Wed, 05 May 2010 15:30:01 +0200 | Cezary Kaliszyk | fminus and some more theorems ported from Finite_Set. | file | diff | annotate |
| Tue, 04 May 2010 16:25:16 +0200 | Cezary Kaliszyk | Translating lemmas from Finite_Set to FSet. | file | diff | annotate |