| Tue, 27 Mar 2012 15:34:04 +0200 | bulwahn | merged | changeset | files |
| Tue, 27 Mar 2012 14:14:46 +0200 | bulwahn | association lists with distinct keys uses the quotient infrastructure to obtain code certificates; | changeset | files |
| Tue, 27 Mar 2012 14:49:56 +0200 | huffman | remove redundant lemmas | changeset | files |
| Tue, 27 Mar 2012 12:42:54 +0200 | huffman | move int::ring_div instance upward, simplify several proofs | changeset | files |
| Tue, 27 Mar 2012 11:45:02 +0200 | huffman | rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names | changeset | files |
| Tue, 27 Mar 2012 11:41:16 +0200 | huffman | extend definition of divmod_int_rel to handle denominator=0 case | changeset | files |