Nominal/Nominal2_FCB.thy
2018-04-19 Christian Urban updated to Isabelle 2016-1 default
2014-03-13 Christian Urban updated to changes in Isabelle
2013-04-18 Christian Urban updated to simplifier changes
2012-07-12 Christian Urban streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
2012-06-04 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
2012-01-16 Christian Urban commented out parts of TypeScheme1 in order to run all tests
2012-01-04 Christian Urban added an FCB for res (will not define evry function, but is a good datapoint)
2011-07-05 Christian Urban added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.
2011-07-05 Christian Urban all FCB lemmas
less more (0) tip