:: deftheorem defines IndexedREAL HUFFMAN1:def 1 :
IndexedREAL = [:NAT,REAL:];