Thu, 23 Aug 2007 18:52:44 +0200 import BinInduct;
huffman [Thu, 23 Aug 2007 18:52:44 +0200] rev 24413
import BinInduct; remove constant bin_rl; remove redundant lemmas and definitions; clean up some proofs
Thu, 23 Aug 2007 18:47:08 +0200 declare bin_rest_BIT_bin_last [simp]
huffman [Thu, 23 Aug 2007 18:47:08 +0200] rev 24412
declare bin_rest_BIT_bin_last [simp]
Thu, 23 Aug 2007 16:47:16 +0200 Word/BinInduct.thy
huffman [Thu, 23 Aug 2007 16:47:16 +0200] rev 24411
Word/BinInduct.thy
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip