haftmann [Tue, 02 Nov 2010 16:48:19 +0100] rev 40549
tuned proof
haftmann [Tue, 02 Nov 2010 16:36:33 +0100] rev 40548
tuned lemma proposition of properties_for_sort_key
haftmann [Tue, 02 Nov 2010 16:31:57 +0100] rev 40547
lemmas sorted_map_same, sorted_same
haftmann [Tue, 02 Nov 2010 16:31:56 +0100] rev 40546
lemmas multiset_of_filter, sort_key_by_quicksort
wenzelm [Tue, 02 Nov 2010 20:16:56 +0100] rev 40545
avoid catch-all exception handling;
wenzelm [Tue, 02 Nov 2010 20:15:57 +0100] rev 40544
eliminated fragile catch-all pattern, based on educated guess about the intended exception;
traytel [Tue, 02 Nov 2010 12:37:12 +0100] rev 40543
Attribute map_function -> coercion_map;
tuned;
wenzelm [Sun, 31 Oct 2010 13:26:37 +0100] rev 40542
syntax category "real" subsumes plain "int";
nipkow [Sun, 31 Oct 2010 11:45:45 +0100] rev 40541
merged
nipkow [Fri, 29 Oct 2010 17:57:36 +0200] rev 40540
Plus -> Sum_Type.Plus