Nominal/nominal_library.ML
2010-12-22 Christian Urban a bit tuning
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-17 Christian Urban tuned
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-14 Christian Urban freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
2010-12-12 Christian Urban created strong_exhausts terms
2010-12-12 Christian Urban moved setify and listify functions into the library; introduced versions that have a type argument
less more (0) -10 -7 tip