| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
TFF: declare free types as types
|
changeset |
files
|
| 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
|
| 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
|
| Mon, 26 Mar 2012 21:03:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 26 Mar 2012 21:00:39 +0200 |
nipkow |
merged
|
changeset |
files
|