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 |
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 |
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 |
Sun, 29 Aug 2010 01:17:36 +0800 | Christian Urban | added proofs for fsupp properties | file | diff | annotate |
Sun, 29 Aug 2010 00:09:45 +0800 | Christian Urban | proved supports lemmas | file | diff | annotate |
Sat, 28 Aug 2010 13:41:31 +0800 | Christian Urban | updated to new Isabelle | file | diff | annotate |