| Fri, 27 Aug 2010 03:37:17 +0800 |
Christian Urban |
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 02:03:52 +0800 |
Christian Urban |
corrected bug with fv-function generation (that was the problem with recursive binders)
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 23:16:42 +0800 |
Christian Urban |
cleaning of unused files and code
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:02:06 +0800 |
Christian Urban |
can now deal with type variables in nominal datatype definitions
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 17:52:25 +0800 |
Christian Urban |
improved code
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 06:39:27 +0800 |
Christian Urban |
added rsp-lemmas for alpha_bns
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 11:03:13 +0800 |
Christian Urban |
simplified code
|
file |
diff |
annotate
|
| Sat, 14 Aug 2010 16:54:41 +0800 |
Christian Urban |
more experiments with lifting
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 19:53:57 +0800 |
Christian Urban |
rsp for constructors
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 16:21:24 +0800 |
Christian Urban |
added a function that transforms the helper-rsp lemmas into real rsp lemmas
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 10:12:38 +0800 |
Christian Urban |
proved rsp-helper lemmas of size functions
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 02:10:42 +0100 |
Christian Urban |
tuning
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 02:05:25 +0100 |
Christian Urban |
further simplification with alpha_prove
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 01:24:39 +0100 |
Christian Urban |
introduced a general alpha_prove method
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 10:16:33 +0100 |
Christian Urban |
helper lemmas for rsp-lemmas
|
file |
diff |
annotate
|