| 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 |
| Tue, 27 Mar 2012 11:02:18 +0200 | huffman | tuned proofs | changeset | files |
| Tue, 27 Mar 2012 10:34:12 +0200 | huffman | shorten a proof | changeset | files |
| Tue, 27 Mar 2012 10:20:31 +0200 | huffman | simplify some proofs | changeset | files |
| Tue, 27 Mar 2012 09:54:39 +0200 | huffman | rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc. | changeset | files |
| Tue, 27 Mar 2012 09:44:56 +0200 | huffman | simplify some proofs | changeset | files |