Sat, 14 Aug 2010 23:33:23 +0800 |
Christian Urban |
improved code
|
changeset |
files
|
Sat, 14 Aug 2010 16:54:41 +0800 |
Christian Urban |
more experiments with lifting
|
changeset |
files
|
Thu, 12 Aug 2010 21:29:35 +0800 |
Christian Urban |
updated to Isabelle 12th Aug
|
changeset |
files
|
Wed, 11 Aug 2010 19:53:57 +0800 |
Christian Urban |
rsp for constructors
|
changeset |
files
|
Wed, 11 Aug 2010 16:23:50 +0800 |
Christian Urban |
updated to Isabelle 11 Aug
|
changeset |
files
|
Wed, 11 Aug 2010 16:21:24 +0800 |
Christian Urban |
added a function that transforms the helper-rsp lemmas into real rsp lemmas
|
changeset |
files
|
Sun, 08 Aug 2010 10:12:38 +0800 |
Christian Urban |
proved rsp-helper lemmas of size functions
|
changeset |
files
|
Sat, 31 Jul 2010 02:10:42 +0100 |
Christian Urban |
tuning
|
changeset |
files
|
Sat, 31 Jul 2010 02:05:25 +0100 |
Christian Urban |
further simplification with alpha_prove
|
changeset |
files
|
Sat, 31 Jul 2010 01:24:39 +0100 |
Christian Urban |
introduced a general alpha_prove method
|
changeset |
files
|
Fri, 30 Jul 2010 00:40:32 +0100 |
Christian Urban |
equivariance for size
|
changeset |
files
|
Thu, 29 Jul 2010 10:16:33 +0100 |
Christian Urban |
helper lemmas for rsp-lemmas
|
changeset |
files
|
Tue, 27 Jul 2010 23:34:30 +0200 |
Christian Urban |
tests
|
changeset |
files
|
Tue, 27 Jul 2010 14:37:59 +0200 |
Christian Urban |
cleaned up a bit Abs.thy
|
changeset |
files
|
Tue, 27 Jul 2010 09:09:02 +0200 |
Christian Urban |
fixed order of fold_union to make alpha and fv agree
|
changeset |
files
|