Thu, 18 Mar 2010 09:31:31 +0100 |
Christian Urban |
simplified strong induction proof by using flip
|
changeset |
files
|
Thu, 18 Mar 2010 08:32:55 +0100 |
Cezary Kaliszyk |
Rename bound variables + minor cleaning.
|
changeset |
files
|
Thu, 18 Mar 2010 08:03:42 +0100 |
Cezary Kaliszyk |
Move most of the exporting out of the parser.
|
changeset |
files
|
Thu, 18 Mar 2010 07:43:44 +0100 |
Cezary Kaliszyk |
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
|
changeset |
files
|
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
|