added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
This repository contain a new implementation of
Nominal Isabelle.
Subdirectories:
===============
Nominal       ... main files for new Nominal Isabelle
Nominal/Ex    ... examples for new implementation
Outher Subdirectories:
======================
Attic         ... old version of the quotient package (is now 
                  part of the Isabelle distribution)
Literature    ... some relevant papers about binders and
                  Core-Haskell
Paper         ... submitted to ESOP
Pearl         ... accepted at ITP 
Pearl-jv      ... journal version
Quotient-Paper .. accepted to SAC
Slides        ... various talks Christian gave recently