| Mon, 25 Jan 2010 17:53:08 +0100 |
Christian Urban |
cleaned some theorems
|
file |
diff |
annotate
|
| Thu, 21 Jan 2010 19:52:46 +0100 |
Cezary Kaliszyk |
Changed fun_map and rel_map to definitions.
|
file |
diff |
annotate
|
| Thu, 21 Jan 2010 11:11:22 +0100 |
Cezary Kaliszyk |
Automatic cleaning of Bexeq<->Ex1 theorems.
|
file |
diff |
annotate
|
| Thu, 21 Jan 2010 10:55:09 +0100 |
Cezary Kaliszyk |
Using Bexeq_rsp, and manually lifted lemma with Ex1.
|
file |
diff |
annotate
|
| 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
|
| Thu, 10 Dec 2009 12:25:12 +0100 |
Cezary Kaliszyk |
Regularized the hard lemma.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 11:19:34 +0100 |
Cezary Kaliszyk |
Simplification of Babses for regularize; will probably become injection
|
file |
diff |
annotate
|
| Wed, 09 Dec 2009 22:43:11 +0100 |
Cezary Kaliszyk |
Finished one proof in IntEx2.
|
file |
diff |
annotate
|