| Mon, 20 Sep 2010 21:52:45 +0800 |
Christian Urban |
introduced a general procedure for structural inductions; simplified reflexivity proof
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 22:46:40 +0800 |
Christian Urban |
tuned code
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 05:56:49 +0800 |
Christian Urban |
tuned (to conform with indentation policy of Markus)
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 09:17:40 +0800 |
Christian Urban |
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 06:48:14 +0800 |
Christian Urban |
renamed alpha_gen -> alpha_set and Abs -> Abs_set etc
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 22:22:43 +0800 |
Christian Urban |
made the fv-definition aggree more with alpha (needed in the support proofs)
|
file |
diff |
annotate
|
| 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
|