| Mon, 27 Sep 2010 12:19:17 -0400 |
Christian Urban |
added postprocessed fresh-lemmas for constructors
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 09:51:15 -0400 |
Christian Urban |
post-processed eq_iff and supp threormes according to the fv-supp equality
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 04:56:28 -0400 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
| Sat, 25 Sep 2010 08:38:04 -0400 |
Christian Urban |
lifted size_thms and exported them as <name>.size
|
file |
diff |
annotate
|
| Sat, 25 Sep 2010 08:28:45 -0400 |
Christian Urban |
cleaned up two examples
|
file |
diff |
annotate
|
| Sat, 18 Sep 2010 06:09:43 +0800 |
Christian Urban |
updated to Isabelle Sept 16
|
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
|
| Sun, 05 Sep 2010 07:00:19 +0800 |
Christian Urban |
generated inducts rule by Project_Rule.projections
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 06:42:53 +0800 |
Christian Urban |
added the definition supp_rel (support w.r.t. a relation)
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 06:23:31 +0800 |
Christian Urban |
moved a proof to Abs
|
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
|
| Thu, 02 Sep 2010 18:10:06 +0800 |
Christian Urban |
some experiments with support
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 12:14:40 +0800 |
Christian Urban |
updated todos
|
file |
diff |
annotate
|