Wed, 27 Sep 2006 01:35:25 +0200 huffman reorganize section headings
Wed, 27 Sep 2006 01:18:35 +0200 huffman more lemmas about Standard and star_of
Wed, 27 Sep 2006 00:54:10 +0200 huffman define new constant Standard = range star_of
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip