| Fri, 15 Jan 2010 16:13:49 +0100 |
Christian Urban |
tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
|
changeset |
files
|
| Fri, 15 Jan 2010 15:56:25 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Fri, 15 Jan 2010 15:56:06 +0100 |
Christian Urban |
added free_variable function (do not know about the algorithm yet)
|
changeset |
files
|
| Fri, 15 Jan 2010 15:51:25 +0100 |
Cezary Kaliszyk |
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
|
changeset |
files
|
| Fri, 15 Jan 2010 12:17:30 +0100 |
Christian Urban |
slight tuning of relation_error
|
changeset |
files
|
| Fri, 15 Jan 2010 11:04:21 +0100 |
Cezary Kaliszyk |
Appropriate respects and a statement of the lifted hom lemma
|
changeset |
files
|
| Fri, 15 Jan 2010 10:48:49 +0100 |
Christian Urban |
recursion-hom for lambda
|
changeset |
files
|
| Fri, 15 Jan 2010 10:36:48 +0100 |
Cezary Kaliszyk |
Incorrect version of the homomorphism lemma
|
changeset |
files
|
| Thu, 14 Jan 2010 23:51:17 +0100 |
Christian Urban |
trivial
|
changeset |
files
|
| Thu, 14 Jan 2010 23:48:31 +0100 |
Christian Urban |
tuned quotient_typ.ML
|
changeset |
files
|
| Thu, 14 Jan 2010 23:17:21 +0100 |
Christian Urban |
tuned quotient_def.ML and cleaned somewhat LamEx.thy
|
changeset |
files
|
| Thu, 14 Jan 2010 19:03:08 +0100 |
Christian Urban |
a few more lemmas...except supp of lambda-abstractions
|
changeset |
files
|