| 2011-05-10 | Christian Urban | updated to new Isabelle (> 9 May) | file | diff | annotate |
| 2011-05-03 | Christian Urban | proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) | file | diff | annotate |
| 2010-12-22 | Christian Urban | properly exported strong exhaust theorem; cleaned up some examples | 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-11-06 | Christian Urban | added a test about subtyping; disabled two tests, because of problem with function package | file | diff | annotate |
| 2010-09-25 | Christian Urban | added example about datatypes | file | diff | annotate |