| Sat, 24 Oct 2009 14:00:18 +0200 |
Cezary Kaliszyk |
Finally completely lift the previously lifted theorems + clean some old stuff
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 13:00:54 +0200 |
Cezary Kaliszyk |
More infrastructure for automatic lifting of theorems lifted before
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 10:16:53 +0200 |
Cezary Kaliszyk |
More infrastructure for automatic lifting of theorems lifted before
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 08:09:09 +0200 |
cek |
Better tactic and simplified the proof further
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:01:13 +0200 |
Cezary Kaliszyk |
eqsubst_tac
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 15:44:16 +0200 |
Cezary Kaliszyk |
Removed an assumption
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 15:02:01 +0200 |
Cezary Kaliszyk |
The proof now including manually unfolded higher-order RES_FORALL_RSP.
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:45:48 +0200 |
Cezary Kaliszyk |
The problems with 'abs' term.
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 16:06:54 +0200 |
Cezary Kaliszyk |
Partial simplification of the proof
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 17:05:52 +0200 |
Cezary Kaliszyk |
Symmetric version of REP_ABS_RSP
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 16:51:01 +0200 |
Cezary Kaliszyk |
Progressing with the proof
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 10:25:23 +0200 |
Cezary Kaliszyk |
A number of lemmas for REGULARIZE_TAC and regularizing card1.
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 18:13:16 +0200 |
Cezary Kaliszyk |
Proving the proper RepAbs version
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 16:23:32 +0200 |
Cezary Kaliszyk |
Manually regularized list_induct2
|
file |
diff |
annotate
|
| Tue, 11 Aug 2009 12:29:15 +0200 |
Christian Urban |
initial commit
|
file |
diff |
annotate
|