Nominal/Ex/Foo2.thy
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
2010-12-06 Christian Urban automated alpha_perm_bn theorems
2010-12-06 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-12-03 Christian Urban updated to Isabelle 2nd December
2010-11-29 Christian Urban isarfied some of the high-level proofs
2010-11-29 Christian Urban added abs_rename_res lemma
2010-11-29 Christian Urban completed proofs in Foo2
2010-11-28 Christian Urban completed the strong exhausts rules for Foo2 using general lemmas
2010-11-27 Christian Urban disabled the Foo examples, because of heavy work
2010-11-26 Christian Urban slightly simplified the Foo2 tests and hint at a general lemma
2010-11-26 Christian Urban completely different method fro deriving the exhaust lemma
2010-11-26 Cezary Kaliszyk missing freshness assumptions
2010-11-25 Cezary Kaliszyk foo2 strong induction
2010-11-24 Cezary Kaliszyk foo2 full exhausts
2010-11-24 Cezary Kaliszyk Foo2 strong_exhaust for first variable.
2010-11-22 Cezary Kaliszyk single rename in let2
2010-11-21 Christian Urban added example Foo2.thy
less more (0) tip