2018-04-19 |
Christian Urban |
updated to Isabelle 2016-1
default
|
file |
diff |
annotate
|
2016-03-19 |
Christian Urban |
updated to Isabelle 2016
Nominal2-Isabelle2016
|
file |
diff |
annotate
|
2015-07-09 |
Christian Urban |
updated for Isabelle 2015
|
file |
diff |
annotate
|
2014-07-07 |
Christian Urban |
changed add.assoc
|
file |
diff |
annotate
|
2014-05-19 |
Christian Urban |
changes from upstream
|
file |
diff |
annotate
|
2014-05-16 |
Christian Urban |
updated changes from upstream (AFP)
|
file |
diff |
annotate
|
2014-03-24 |
Christian Urban |
updated to massive changes in Isabelle
|
file |
diff |
annotate
|
2014-03-13 |
Christian Urban |
updated to Isabelle changes
|
file |
diff |
annotate
|
2013-12-15 |
Christian Urban |
updated to changes in Isabelle
|
file |
diff |
annotate
|
2013-09-06 |
Christian Urban |
restricted fresh_ineq simproc so that it is faster
|
file |
diff |
annotate
|
2013-07-31 |
Christian Urban |
added some lemmas
|
file |
diff |
annotate
|
2013-06-04 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
2013-04-18 |
Christian Urban |
updated to simplifier changes
|
file |
diff |
annotate
|
2013-03-27 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
2013-03-27 |
webertj |
Various changes to support Nominal2 commands in local contexts.
|
file |
diff |
annotate
|
2013-03-26 |
webertj |
Manual merge of d121bd2a5a47 from Isabelle/AFP.
|
file |
diff |
annotate
|
2012-10-19 |
Christian Urban |
updated to changes in the type-def package
|
file |
diff |
annotate
|
2012-10-04 |
Christian Urban |
removed "use" - replaced by "ML_file"
|
file |
diff |
annotate
|
2012-08-07 |
Christian Urban |
definition of an auxiliary graph in nominal-primrec definitions
|
file |
diff |
annotate
|
2012-08-07 |
Christian Urban |
added eqvt-lemma for function composition
|
file |
diff |
annotate
|
2012-07-12 |
Christian Urban |
streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
|
file |
diff |
annotate
|
2012-06-12 |
Christian Urban |
added eqvt for finfun_apply
|
file |
diff |
annotate
|
2012-06-12 |
Christian Urban |
improved the finfun parts
|
file |
diff |
annotate
|
2012-06-12 |
Christian Urban |
added finfun-type to Nominal
|
file |
diff |
annotate
|
2012-06-09 |
Christian Urban |
added a rule about inequality of freshness between atoms to the simplifier
|
file |
diff |
annotate
|
2012-06-06 |
Christian Urban |
a simproc for simplifying Fresh when there is a sufficiently fresh atom
|
file |
diff |
annotate
|
2012-06-04 |
Christian Urban |
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
|
file |
diff |
annotate
|
2012-05-31 |
Christian Urban |
added let-eqvt back
|
file |
diff |
annotate
|