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-11-07 |
Christian Urban |
fixed locally the problem with the function package; all tests work again
|
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 |
supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
|
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-28 |
Christian Urban |
added proofs for fsupp properties
|
file |
diff |
annotate
|
2010-08-28 |
Christian Urban |
proved supports lemmas
|
file |
diff |
annotate
|
2010-08-28 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
2010-08-19 |
Christian Urban |
used @{const_name} hopefully everywhere
|
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 |
deleted unused code
|
file |
diff |
annotate
|
2010-08-17 |
Christian Urban |
improved code
|
file |
diff |
annotate
|
2010-08-15 |
Christian Urban |
simplified code
|
file |
diff |
annotate
|
2010-08-14 |
Christian Urban |
improved code
|
file |
diff |
annotate
|
2010-08-14 |
Christian Urban |
more experiments with lifting
|
file |
diff |
annotate
|
2010-07-31 |
Christian Urban |
introduced a general alpha_prove method
|
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-09 |
Christian Urban |
transitivity proofs done
|
file |
diff |
annotate
|
2010-06-07 |
Christian Urban |
work on transitivity proof
|
file |
diff |
annotate
|
2010-05-31 |
Christian Urban |
all raw definitions are defined using function
|
file |
diff |
annotate
|
2010-05-24 |
Christian Urban |
alpha works now
|
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
|
2010-04-29 |
Christian Urban |
added basic functions for constructing supp-terms
|
file |
diff |
annotate
|
2010-04-27 |
Christian Urban |
some tuning
|
file |
diff |
annotate
|
2010-04-27 |
Christian Urban |
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
|
file |
diff |
annotate
|
2010-04-20 |
Christian Urban |
optimised the code of define_raw_perm
|
file |
diff |
annotate
|
2010-04-19 |
Christian Urban |
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
|
file |
diff |
annotate
|
2010-04-18 |
Christian Urban |
moved some general function into nominal_library.ML
|
file |
diff |
annotate
|
2010-04-14 |
Christian Urban |
moved a couple of more functions to the library
|
file |
diff |
annotate
|
2010-04-14 |
Christian Urban |
added a library for basic nominal functions; separated nominal_eqvt file
|
file |
diff |
annotate
|