Thu, 18 Mar 2010 07:35:44 +0100 |
Cezary Kaliszyk |
Prove eqvts on exported terms.
|
changeset |
files
|
Thu, 18 Mar 2010 07:26:36 +0100 |
Cezary Kaliszyk |
Clean 'Lift', start working only on exported things in Parser.
|
changeset |
files
|
Thu, 18 Mar 2010 00:17:21 +0100 |
Christian Urban |
slightly more of the paper
|
changeset |
files
|
Wed, 17 Mar 2010 20:42:42 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Wed, 17 Mar 2010 20:42:22 +0100 |
Christian Urban |
paper uses now a heap file - does not compile so long anymore
|
changeset |
files
|
Wed, 17 Mar 2010 18:53:23 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Wed, 17 Mar 2010 18:52:59 +0100 |
Cezary Kaliszyk |
compose_sym2 works also for term5
|
changeset |
files
|
Wed, 17 Mar 2010 17:59:04 +0100 |
Cezary Kaliszyk |
Updated Term1, including statement of strong induction.
|
changeset |
files
|
Wed, 17 Mar 2010 17:40:14 +0100 |
Cezary Kaliszyk |
Proper compose_sym2
|
changeset |
files
|
Wed, 17 Mar 2010 17:11:23 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Wed, 17 Mar 2010 17:10:19 +0100 |
Christian Urban |
temporarily disabled tests in Nominal/ROOT
|
changeset |
files
|
Wed, 17 Mar 2010 15:13:31 +0100 |
Christian Urban |
made paper to compile
|
changeset |
files
|
Wed, 17 Mar 2010 15:13:03 +0100 |
Christian Urban |
added partial proof for the strong induction principle
|
changeset |
files
|
Wed, 17 Mar 2010 17:09:01 +0100 |
Cezary Kaliszyk |
Trying to find a compose lemma for 2 arguments.
|
changeset |
files
|
Wed, 17 Mar 2010 12:23:04 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|