Thu, 23 Feb 2012 18:14:58 +0100 wenzelm tuned;
Thu, 23 Feb 2012 17:27:37 +0100 huffman merged
Thu, 23 Feb 2012 16:09:16 +0100 huffman make more simp rules respect int/bin distinction
Thu, 23 Feb 2012 15:37:42 +0100 huffman make bool list functions respect int/bin distinction
Thu, 23 Feb 2012 16:18:19 +0100 wenzelm merged;
Thu, 23 Feb 2012 16:02:07 +0100 wenzelm tuned;
Thu, 23 Feb 2012 15:49:40 +0100 wenzelm clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
Thu, 23 Feb 2012 15:15:59 +0100 wenzelm further graph operations from ML;
Thu, 23 Feb 2012 14:46:38 +0100 wenzelm removed dead code;
Thu, 23 Feb 2012 14:17:51 +0100 wenzelm directed graphs (in Scala);
Thu, 23 Feb 2012 15:23:16 +0100 huffman make uses of bin_split respect int/bin distinction
Thu, 23 Feb 2012 15:19:31 +0100 huffman remove lemma bin_cat_Pls, which doesn't respect int/bin distinction
(0) -30000 -10000 -3000 -1000 -300 -100 -12 +12 +100 +300 +1000 +3000 +10000 +30000 tip