Fri, 08 Jan 2010 11:20:12 +0100 |
Cezary Kaliszyk |
Experimients with fconcat_insert
|
changeset |
files
|
Fri, 08 Jan 2010 10:44:30 +0100 |
Cezary Kaliszyk |
Modifications for new_equiv_rel, part2
|
changeset |
files
|
Fri, 08 Jan 2010 10:39:08 +0100 |
Cezary Kaliszyk |
Modifictaions for new_relation.
|
changeset |
files
|
Fri, 08 Jan 2010 10:08:01 +0100 |
Cezary Kaliszyk |
Proved concat_empty.
|
changeset |
files
|
Thu, 07 Jan 2010 16:51:38 +0100 |
Cezary Kaliszyk |
Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
|
changeset |
files
|
Thu, 07 Jan 2010 16:06:13 +0100 |
Cezary Kaliszyk |
some cleaning.
|
changeset |
files
|
Thu, 07 Jan 2010 15:50:22 +0100 |
Cezary Kaliszyk |
First generalization.
|
changeset |
files
|
Thu, 07 Jan 2010 14:14:17 +0100 |
Cezary Kaliszyk |
The working proof of the special case.
|
changeset |
files
|
Thu, 07 Jan 2010 10:55:20 +0100 |
Cezary Kaliszyk |
Reduced the proof to two simple but not obvious to prove facts.
|
changeset |
files
|
Thu, 07 Jan 2010 10:13:15 +0100 |
Cezary Kaliszyk |
More cleaning and commenting AbsRepTest. Now tests work; just slow.
|
changeset |
files
|
Thu, 07 Jan 2010 09:55:42 +0100 |
Cezary Kaliszyk |
cleaning in AbsRepTest.
|
changeset |
files
|
Wed, 06 Jan 2010 16:24:21 +0100 |
Cezary Kaliszyk |
Further in the proof
|
changeset |
files
|
Wed, 06 Jan 2010 09:19:23 +0100 |
Cezary Kaliszyk |
Tried to prove the lemma manually; only left with quotient proofs.
|
changeset |
files
|
Wed, 06 Jan 2010 08:24:37 +0100 |
Cezary Kaliszyk |
Sledgehammer bug.
|
changeset |
files
|
Tue, 05 Jan 2010 18:10:20 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|