| Thu, 21 Jan 2010 09:55:05 +0100 |
Cezary Kaliszyk |
Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
|
file |
diff |
annotate
|
| Fri, 15 Jan 2010 15:51:25 +0100 |
Cezary Kaliszyk |
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 22:36:21 +0100 |
Christian Urban |
added an abbreviation for OOO
|
file |
diff |
annotate
|
| Fri, 08 Jan 2010 10:39:08 +0100 |
Cezary Kaliszyk |
Modifictaions for new_relation.
|
file |
diff |
annotate
|
| Fri, 08 Jan 2010 10:08:01 +0100 |
Cezary Kaliszyk |
Proved concat_empty.
|
file |
diff |
annotate
|
| Tue, 05 Jan 2010 14:09:04 +0100 |
Christian Urban |
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 17:59:29 +0100 |
Cezary Kaliszyk |
More name and indentation cleaning.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 18:28:30 +0100 |
Christian Urban |
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
|
file |
diff |
annotate
|