Mon, 07 Dec 2009 15:18:44 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Mon, 07 Dec 2009 15:18:00 +0100 |
Cezary Kaliszyk |
make_inst for lambda_prs where the second quotient is not identity.
|
changeset |
files
|
Mon, 07 Dec 2009 14:37:10 +0100 |
Christian Urban |
added "end" to each example theory
|
changeset |
files
|
Mon, 07 Dec 2009 14:35:45 +0100 |
Cezary Kaliszyk |
List moved after QuotMain
|
changeset |
files
|
Mon, 07 Dec 2009 14:14:07 +0100 |
Christian Urban |
cleaning
|
changeset |
files
|
Mon, 07 Dec 2009 14:12:29 +0100 |
Christian Urban |
final move
|
changeset |
files
|
Mon, 07 Dec 2009 14:09:50 +0100 |
Christian Urban |
directory re-arrangement
|
changeset |
files
|
Mon, 07 Dec 2009 14:00:36 +0100 |
Cezary Kaliszyk |
inj_repabs_tac handles Babs now.
|
changeset |
files
|
Mon, 07 Dec 2009 12:14:25 +0100 |
Cezary Kaliszyk |
Fix of regularize for babs and proof of babs_rsp.
|
changeset |
files
|
Mon, 07 Dec 2009 11:14:21 +0100 |
Cezary Kaliszyk |
Using pair_prs; debugging the error in regularize of a lambda.
|
changeset |
files
|
Mon, 07 Dec 2009 08:45:04 +0100 |
Cezary Kaliszyk |
QuotProd with product_quotient and a 3 respects and preserves lemmas.
|
changeset |
files
|
Mon, 07 Dec 2009 04:41:42 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|