Tutorial/Lambda.thy
2014-05-19 Christian Urban changed nominal_primrec to nominal_function and termination to nominal_termination
2014-05-19 Christian Urban changed nominal_primrec into the more appropriate nominal_function
2012-08-07 Christian Urban definition of an auxiliary graph in nominal-primrec definitions
2012-07-15 Christian Urban added a simproc for alpha-equivalence to the simplifier
2012-06-04 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
2012-03-05 Christian Urban updated tutorial to latest version and added it to the tests
2011-02-04 Christian Urban Lambda.thy which works with Nominal_Isabelle2011
2011-01-23 Christian Urban cleaning up
2011-01-19 Christian Urban added a very rough version of the tutorial; all seems to work
2011-01-19 Christian Urban base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
less more (0) tip