| Tue, 28 Jun 2011 14:49:48 +0100 |
Christian Urban |
relaxed type in fcb
|
changeset |
files
|
| Tue, 28 Jun 2011 14:34:07 +0100 |
Christian Urban |
fcb with explicit bn function
|
changeset |
files
|
| Tue, 28 Jun 2011 14:01:52 +0100 |
Christian Urban |
added let-rec example
|
changeset |
files
|
| Tue, 28 Jun 2011 12:36:34 +0900 |
Cezary Kaliszyk |
Experiments with res
|
changeset |
files
|
| Tue, 28 Jun 2011 00:48:57 +0100 |
Christian Urban |
proved the fcb also for sets (no restriction yet)
|
changeset |
files
|
| Tue, 28 Jun 2011 00:30:30 +0100 |
Christian Urban |
copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
|
changeset |
files
|
| Mon, 27 Jun 2011 22:51:42 +0100 |
Christian Urban |
streamlined the fcb-proof and made fcb1 a special case of fcb
|
changeset |
files
|
| Mon, 27 Jun 2011 19:22:10 +0100 |
Christian Urban |
completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier)
|
changeset |
files
|
| Mon, 27 Jun 2011 19:15:18 +0100 |
Christian Urban |
fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.
|
changeset |
files
|
| Mon, 27 Jun 2011 19:13:55 +0100 |
Christian Urban |
renamed ds to dset (disagreement set)
|
changeset |
files
|
| Mon, 27 Jun 2011 12:15:21 +0100 |
Christian Urban |
added small lemma about disagreement set
|
changeset |
files
|
| Mon, 27 Jun 2011 08:42:02 +0900 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Mon, 27 Jun 2011 08:38:54 +0900 |
Cezary Kaliszyk |
New-style fcb for multiple binders.
|
changeset |
files
|
| Mon, 27 Jun 2011 04:01:55 +0900 |
Cezary Kaliszyk |
equality of lst_binder and a few helper lemmas
|
changeset |
files
|
| Sun, 26 Jun 2011 21:42:07 +0100 |
Christian Urban |
only one of the fcb precondistions are needed (probably the same with the perm-conditions)
|
changeset |
files
|