Sat, 15 Mar 2014 08:31:33 +0100 | haftmann | more complete set of lemmas wrt. image and composition | file | diff | annotate |
Sun, 16 Feb 2014 21:33:28 +0100 | blanchet | folded 'list_all2' with the relator generated by 'datatype_new' | file | diff | annotate |
Fri, 14 Feb 2014 07:53:46 +0100 | blanchet | merged 'Option.map' and 'Option.map_option' | file | diff | annotate |
Fri, 02 Aug 2013 23:03:59 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
Fri, 27 Jul 2012 19:57:23 +0200 | wenzelm | tuned proofs -- avoid odd situations of polymorphic Frees in goal state; | file | diff | annotate |
Sun, 15 Jan 2012 18:55:27 +0100 | wenzelm | tuned proofs; | 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 |