| Thu, 23 Aug 2007 23:34:51 +0200 | huffman | avoid use of bin_rec_PM | changeset | files |
| Thu, 23 Aug 2007 20:15:45 +0200 | huffman | new instance proofs | changeset | files |
| Thu, 23 Aug 2007 18:53:53 +0200 | huffman | remove unused lemmas | changeset | files |
| Thu, 23 Aug 2007 18:52:44 +0200 | huffman | import BinInduct; | changeset | files |
| Thu, 23 Aug 2007 18:47:08 +0200 | huffman | declare bin_rest_BIT_bin_last [simp] | changeset | files |
| 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 |
| Wed, 22 Aug 2007 21:09:21 +0200 | huffman | removed Word/Size.thy; | changeset | files |
| Wed, 22 Aug 2007 20:59:19 +0200 | huffman | typed print translation for CARD('a); | changeset | files |
| Wed, 22 Aug 2007 18:53:54 +0200 | huffman | rename type pls to num0 | changeset | files |
| Wed, 22 Aug 2007 17:58:37 +0200 | huffman | move constant definitions to their respective subsections | changeset | files |