src/HOL/List.thy
Tue, 31 Jul 2012 13:55:39 +0200 kuncar more set operations expressed by Finite_Set.fold
Mon, 30 Apr 2012 12:14:53 +0200 bulwahn making sorted_list_of_set executable
Sat, 21 Apr 2012 06:49:04 +0200 huffman strengthen rule list_all2_induct
Thu, 12 Apr 2012 11:01:15 +0200 bulwahn merged
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
Fri, 06 Apr 2012 19:23:51 +0200 haftmann abandoned almost redundant *_foldr lemmas
Fri, 06 Apr 2012 19:18:00 +0200 haftmann tuned
Fri, 06 Apr 2012 18:17:16 +0200 haftmann no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
Mon, 26 Mar 2012 21:00:23 +0200 nipkow reverted to canonical name
Mon, 26 Mar 2012 18:54:41 +0200 nipkow Functions and lemmas by Christian Sternagel
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 13 Mar 2012 13:31:26 +0100 wenzelm tuned proofs -- eliminated pointless chaining of facts after 'interpret';
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs
Mon, 27 Feb 2012 09:01:49 +0100 nipkow converting "set [...]" to "{...}" in evaluation results
Sat, 25 Feb 2012 09:07:37 +0100 bulwahn one general list_all2_update_cong instead of two special ones
less more (0) -300 -100 -15 tip