| Thu, 18 Mar 2010 12:09:59 +0100 |
Cezary Kaliszyk |
Added fv,bn,distinct,perm to the simplifier.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 10:12:41 +0100 |
Cezary Kaliszyk |
Which proofs need a 'sorry'.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 10:02:21 +0100 |
Christian Urban |
vixed variable names
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 09:31:31 +0100 |
Christian Urban |
simplified strong induction proof by using flip
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 08:32:55 +0100 |
Cezary Kaliszyk |
Rename bound variables + minor cleaning.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 07:43:44 +0100 |
Cezary Kaliszyk |
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 17:11:23 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 15:13:03 +0100 |
Christian Urban |
added partial proof for the strong induction principle
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 12:23:04 +0100 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 12:18:35 +0100 |
Cezary Kaliszyk |
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 11:53:56 +0100 |
Christian Urban |
added proof of supp/fv for type schemes
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 10:34:25 +0100 |
Christian Urban |
added partial proof of supp for type schemes
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:57:54 +0100 |
Cezary Kaliszyk |
Fix in alpha; support of the recursive Let works :)
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:42:56 +0100 |
Cezary Kaliszyk |
The recursive supp just has one equation too much.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 08:07:25 +0100 |
Christian Urban |
commented out examples that should not work; but for example type-scheme example should work
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 06:49:33 +0100 |
Christian Urban |
added another supp-proof for the non-recursive case
|
file |
diff |
annotate
|