Thu, 23 Aug 2007 16:47:16 +0200 | huffman | Word/BinInduct.thy | changeset | files |
Thu, 23 Aug 2007 16:46:40 +0200 | huffman | theory of integers as an inductive datatype | changeset | files |
Thu, 23 Aug 2007 15:47:42 +0200 | huffman | move bin_nth stuff to its own subsection | changeset | files |