Fri, 23 Dec 2011 15:55:23 +0100 | huffman | remove redundant lemma word_sub_def | changeset | files |
Fri, 23 Dec 2011 15:34:18 +0100 | huffman | add lemmas bin_cat_zero and bin_split_zero | changeset | files |
Fri, 23 Dec 2011 15:24:22 +0100 | huffman | more uses of 'induct arbitrary' | changeset | files |
Fri, 23 Dec 2011 14:37:38 +0100 | huffman | use 'induct arbitrary' instead of universal quantifiers | changeset | files |
Fri, 23 Dec 2011 11:50:12 +0100 | huffman | remove two conflicting simp rules for 'number_of (number_of _)' pattern | changeset | files |
Thu, 22 Dec 2011 12:14:26 +0100 | huffman | add lemma bin_nth_minus1 | changeset | files |