src/HOL/Word/BinInduct.thy
Thu, 23 Aug 2007 18:47:08 +0200 huffman declare bin_rest_BIT_bin_last [simp]
Thu, 23 Aug 2007 16:46:40 +0200 huffman theory of integers as an inductive datatype
less more (0) tip