2012-02-28 |
Cezary Kaliszyk |
Update to the localized quotient package
|
file |
diff |
annotate
|
2012-02-17 |
Cezary Kaliszyk |
Update from Isabelle Wed Feb 15 23:19:30
|
file |
diff |
annotate
|
2011-11-03 |
Christian Urban |
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
|
file |
diff |
annotate
|
2011-09-21 |
Christian Urban |
deleted PNil
|
file |
diff |
annotate
|
2011-07-07 |
Christian Urban |
code refactoring; introduced a record for raw_dt_info
|
file |
diff |
annotate
|
2011-06-30 |
Christian Urban |
more code refactoring
|
file |
diff |
annotate
|
2011-06-29 |
Christian Urban |
combined distributed data for alpha in alpha_result (partially done)
|
file |
diff |
annotate
|
2011-06-29 |
Christian Urban |
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
|
file |
diff |
annotate
|
2011-06-28 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
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-06-16 |
Christian Urban |
got rid of the boolean flag in the raw_equivariance function
|
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-16 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
2010-12-06 |
Christian Urban |
automated alpha_perm_bn theorems
|
file |
diff |
annotate
|
2010-12-06 |
Christian Urban |
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
|
file |
diff |
annotate
|
2010-12-03 |
Christian Urban |
updated to Isabelle 2nd December
|
file |
diff |
annotate
|
2010-11-13 |
Christian Urban |
respectfulness for permute_bn functions
|
file |
diff |
annotate
|
2010-11-12 |
Christian Urban |
automated permute_bn functions (raw ones first)
|
file |
diff |
annotate
|
2010-11-10 |
Christian Urban |
adapted to changes by Florian on the quotient package and removed local fix for function package
|
file |
diff |
annotate
|
2010-09-20 |
Christian Urban |
introduced a general procedure for structural inductions; simplified reflexivity proof
|
file |
diff |
annotate
|
2010-09-12 |
Christian Urban |
tuned code
|
file |
diff |
annotate
|
2010-09-10 |
Christian Urban |
tuned (to conform with indentation policy of Markus)
|
file |
diff |
annotate
|
2010-09-10 |
Christian Urban |
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
|
file |
diff |
annotate
|
2010-09-03 |
Christian Urban |
renamed alpha_gen -> alpha_set and Abs -> Abs_set etc
|
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 |
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
|
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 |
cleaning of unused files and code
|
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 code
|
file |
diff |
annotate
|
2010-08-16 |
Christian Urban |
added rsp-lemmas for alpha_bns
|
file |
diff |
annotate
|
2010-08-15 |
Christian Urban |
simplified code
|
file |
diff |
annotate
|
2010-08-14 |
Christian Urban |
more experiments with lifting
|
file |
diff |
annotate
|
2010-08-11 |
Christian Urban |
rsp for constructors
|
file |
diff |
annotate
|
2010-08-11 |
Christian Urban |
added a function that transforms the helper-rsp lemmas into real rsp lemmas
|
file |
diff |
annotate
|
2010-08-08 |
Christian Urban |
proved rsp-helper lemmas of size functions
|
file |
diff |
annotate
|
2010-07-31 |
Christian Urban |
tuning
|
file |
diff |
annotate
|
2010-07-31 |
Christian Urban |
further simplification with alpha_prove
|
file |
diff |
annotate
|
2010-07-31 |
Christian Urban |
introduced a general alpha_prove method
|
file |
diff |
annotate
|
2010-07-29 |
Christian Urban |
helper lemmas for rsp-lemmas
|
file |
diff |
annotate
|
2010-07-27 |
Christian Urban |
cleaned up a bit Abs.thy
|
file |
diff |
annotate
|
2010-07-19 |
Christian Urban |
minor polishing
|
file |
diff |
annotate
|
2010-06-22 |
Christian Urban |
proved eqvip theorems for alphas
|
file |
diff |
annotate
|
2010-06-22 |
Christian Urban |
prove that alpha implies alpha_bn (needed for rsp proofs)
|
file |
diff |
annotate
|
2010-06-11 |
Christian Urban |
also symmetry
|
file |
diff |
annotate
|
2010-06-10 |
Christian Urban |
premerge
|
file |
diff |
annotate
|
2010-06-09 |
Christian Urban |
transitivity proofs done
|
file |
diff |
annotate
|
2010-06-07 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
2010-05-26 |
Christian Urban |
added FSet to the correct paper
|
file |
diff |
annotate
|
2010-05-24 |
Christian Urban |
added slides
|
file |
diff |
annotate
|
2010-05-24 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2010-05-24 |
Christian Urban |
tuned
|
file |
diff |
annotate
|