Tue, 27 Dec 2011 15:37:33 +0100 | huffman | redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min | file | diff | annotate |
Tue, 27 Dec 2011 13:16:22 +0100 | huffman | remove some uses of Int.succ and Int.pred | file | diff | annotate |
Tue, 27 Dec 2011 12:49:03 +0100 | huffman | removed unused lemmas | file | diff | annotate |
Fri, 23 Dec 2011 14:37:38 +0100 | huffman | use 'induct arbitrary' instead of universal quantifiers | file | diff | annotate |
Fri, 23 Dec 2011 11:50:12 +0100 | huffman | remove two conflicting simp rules for 'number_of (number_of _)' pattern | file | diff | annotate |
Thu, 22 Dec 2011 12:14:26 +0100 | huffman | add lemma bin_nth_minus1 | file | diff | annotate |
Tue, 13 Dec 2011 18:33:04 +0100 | huffman | more simp rules for sbintrunc | file | diff | annotate |