2011-06-23 |
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
|
2011-04-13 |
Christian Urban |
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
|
file |
diff |
annotate
|
2010-12-28 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
2010-12-21 |
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
|
2010-12-16 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
2010-12-12 |
Christian Urban |
created strong_exhausts terms
|
file |
diff |
annotate
|
2010-12-12 |
Christian Urban |
moved setify and listify functions into the library; introduced versions that have a type argument
|
file |
diff |
annotate
|
2010-12-08 |
Christian Urban |
moved definition of raw bn-functions into nominal_dt_rawfuns
|
file |
diff |
annotate
|
2010-12-07 |
Christian Urban |
automated permute_bn theorems
|
file |
diff |
annotate
|
2010-11-15 |
Christian Urban |
proved that bn functions return a finite set
|
file |
diff |
annotate
|
2010-11-15 |
Christian Urban |
fixed bug in fv function where a shallow binder binds lists of names
|
file |
diff |
annotate
|
2010-11-12 |
Christian Urban |
automated permute_bn functions (raw ones first)
|
file |
diff |
annotate
|
2010-10-17 |
Christian Urban |
all tests work again
|
file |
diff |
annotate
|
2010-10-14 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
2010-09-10 |
Christian Urban |
tuned (to conform with indentation policy of Markus)
|
file |
diff |
annotate
|
2010-09-03 |
Christian Urban |
made the fv-definition aggree more with alpha (needed in the support proofs)
|
file |
diff |
annotate
|
2010-08-26 |
Christian Urban |
corrected bug with fv-function generation (that was the problem with recursive binders)
|
file |
diff |
annotate
|
2010-08-25 |
Christian Urban |
can now deal with type variables in nominal datatype definitions
|
file |
diff |
annotate
|
2010-08-17 |
Christian Urban |
improved runtime slightly, by constructing an explicit size measure for the function definitions
|
file |
diff |
annotate
|
2010-08-17 |
Christian Urban |
more tuning of the code
|
file |
diff |
annotate
|
2010-08-17 |
Christian Urban |
improved code
|
file |
diff |
annotate
|
2010-07-29 |
Christian Urban |
equivariance for size
|
file |
diff |
annotate
|
2010-07-27 |
Christian Urban |
cleaned up a bit Abs.thy
|
file |
diff |
annotate
|
2010-07-27 |
Christian Urban |
fixed order of fold_union to make alpha and fv agree
|
file |
diff |
annotate
|
2010-07-19 |
Christian Urban |
minor polishing
|
file |
diff |
annotate
|
2010-06-22 |
Christian Urban |
cleaned up the FSet (noise was introduced by error)
|
file |
diff |
annotate
|
2010-06-07 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
2010-06-03 |
Christian Urban |
fixed problem with eqvt proofs
|
file |
diff |
annotate
|
2010-06-02 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
2010-06-01 |
Christian Urban |
smaller code for raw-eqvt proofs
|
file |
diff |
annotate
|
2010-05-31 |
Christian Urban |
all raw definitions are defined using function
|
file |
diff |
annotate
|
2010-05-24 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-05-24 |
Christian Urban |
alpha works now
|
file |
diff |
annotate
|
2010-05-23 |
Christian Urban |
started to work on alpha
|
file |
diff |
annotate
|
2010-05-22 |
Christian Urban |
properly exported bn_descr
|
file |
diff |
annotate
|
2010-05-21 |
Christian Urban |
hving a working fv-definition without the export
|
file |
diff |
annotate
|
2010-05-21 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-05-20 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-05-20 |
Christian Urban |
moved some mk_union and mk_diff into the library
|
file |
diff |
annotate
|
2010-05-20 |
Christian Urban |
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
|
file |
diff |
annotate
|