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 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 09:02:06 +0800 |
Christian Urban |
can now deal with type variables in nominal datatype definitions
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 00:19:15 +0800 |
Christian Urban |
improved runtime slightly, by constructing an explicit size measure for the function definitions
|
file |
diff |
annotate
|
Tue, 17 Aug 2010 18:17:53 +0800 |
Christian Urban |
more tuning of the code
|
file |
diff |
annotate
|
Tue, 17 Aug 2010 17:52:25 +0800 |
Christian Urban |
improved code
|
file |
diff |
annotate
|
Fri, 30 Jul 2010 00:40:32 +0100 |
Christian Urban |
equivariance for size
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 14:37:59 +0200 |
Christian Urban |
cleaned up a bit Abs.thy
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 09:09:02 +0200 |
Christian Urban |
fixed order of fold_union to make alpha and fv agree
|
file |
diff |
annotate
|
Mon, 19 Jul 2010 16:59:43 +0100 |
Christian Urban |
minor polishing
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 13:31:42 +0100 |
Christian Urban |
cleaned up the FSet (noise was introduced by error)
|
file |
diff |
annotate
|
Mon, 07 Jun 2010 11:43:01 +0200 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
Thu, 03 Jun 2010 11:48:44 +0200 |
Christian Urban |
fixed problem with eqvt proofs
|
file |
diff |
annotate
|
Wed, 02 Jun 2010 11:37:51 +0200 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
Tue, 01 Jun 2010 15:01:05 +0200 |
Christian Urban |
smaller code for raw-eqvt proofs
|
file |
diff |
annotate
|
Mon, 31 May 2010 19:57:29 +0200 |
Christian Urban |
all raw definitions are defined using function
|
file |
diff |
annotate
|
Mon, 24 May 2010 20:50:15 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
Mon, 24 May 2010 20:02:37 +0100 |
Christian Urban |
alpha works now
|
file |
diff |
annotate
|
Sun, 23 May 2010 02:15:24 +0100 |
Christian Urban |
started to work on alpha
|
file |
diff |
annotate
|
Sat, 22 May 2010 13:51:47 +0100 |
Christian Urban |
properly exported bn_descr
|
file |
diff |
annotate
|
Fri, 21 May 2010 11:40:18 +0100 |
Christian Urban |
hving a working fv-definition without the export
|
file |
diff |
annotate
|
Fri, 21 May 2010 05:58:23 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
Thu, 20 May 2010 21:47:12 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
Thu, 20 May 2010 21:35:00 +0100 |
Christian Urban |
moved some mk_union and mk_diff into the library
|
file |
diff |
annotate
|
Thu, 20 May 2010 21:23:53 +0100 |
Christian Urban |
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
|
file |
diff |
annotate
|