src/HOL/Metis_Examples/Binary_Tree.thy
Tue, 15 Nov 2011 12:39:29 +0100 huffman avoid theorem references like 'semiring_norm(111)'
less more (0) tip