| Thu, 23 Jun 2011 11:30:39 +0100 |
Christian Urban |
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
|
file |
diff |
annotate
|
| Wed, 13 Apr 2011 13:41:52 +0100 |
Christian Urban |
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
|
file |
diff |
annotate
|
| Tue, 28 Dec 2010 19:51:25 +0000 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 10:28:08 +0000 |
Christian Urban |
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 08:42:48 +0000 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 22:09:11 +0000 |
Christian Urban |
created strong_exhausts terms
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 00:10:40 +0000 |
Christian Urban |
moved setify and listify functions into the library; introduced versions that have a type argument
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:05:04 +0000 |
Christian Urban |
moved definition of raw bn-functions into nominal_dt_rawfuns
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:27:39 +0000 |
Christian Urban |
automated permute_bn theorems
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 09:52:29 +0000 |
Christian Urban |
proved that bn functions return a finite set
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 01:10:02 +0000 |
Christian Urban |
fixed bug in fv function where a shallow binder binds lists of names
|
file |
diff |
annotate
|
| Fri, 12 Nov 2010 01:20:53 +0000 |
Christian Urban |
automated permute_bn functions (raw ones first)
|
file |
diff |
annotate
|
| Sun, 17 Oct 2010 15:53:37 +0100 |
Christian Urban |
all tests work again
|
file |
diff |
annotate
|
| Thu, 14 Oct 2010 04:14:22 +0100 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
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, 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
|