Nominal/Ex/Foo2.thy
2011-07-05 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-28 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-26 Christian Urban generated goals for strong induction theorems.
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
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-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
2010-12-08 Christian Urban first tests about exhaust
2010-12-08 Christian Urban moved some code into the nominal_library
2010-12-08 Christian Urban kept the nested structure of constructors (belonging to one datatype)
2010-12-07 Christian Urban moved general theorems into the libraries
2010-12-07 Christian Urban automated permute_bn theorems
less more (0) -15 tip