Nominal/Ex/Foo2.thy
Tue, 05 Jul 2011 18:42:34 +0200 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Tue, 28 Dec 2010 19:51:25 +0000 Christian Urban automated all strong induction lemmas
Tue, 28 Dec 2010 00:20:50 +0000 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
Sun, 26 Dec 2010 16:35:16 +0000 Christian Urban generated goals for strong induction theorems.
Thu, 23 Dec 2010 00:46:06 +0000 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
Tue, 21 Dec 2010 10:28:08 +0000 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
Thu, 16 Dec 2010 08:42:48 +0000 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
Tue, 14 Dec 2010 14:23:40 +0000 Christian Urban freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
Sun, 12 Dec 2010 22:09:11 +0000 Christian Urban created strong_exhausts terms
Sun, 12 Dec 2010 00:10:40 +0000 Christian Urban moved setify and listify functions into the library; introduced versions that have a type argument
Wed, 08 Dec 2010 17:07:08 +0000 Christian Urban first tests about exhaust
Wed, 08 Dec 2010 13:16:25 +0000 Christian Urban moved some code into the nominal_library
Wed, 08 Dec 2010 12:37:25 +0000 Christian Urban kept the nested structure of constructors (belonging to one datatype)
Tue, 07 Dec 2010 19:16:09 +0000 Christian Urban moved general theorems into the libraries
Tue, 07 Dec 2010 14:27:39 +0000 Christian Urban automated permute_bn theorems
Mon, 06 Dec 2010 16:35:42 +0000 Christian Urban automated alpha_perm_bn theorems
Mon, 06 Dec 2010 14:24:17 +0000 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Fri, 03 Dec 2010 13:51:07 +0000 Christian Urban updated to Isabelle 2nd December
Mon, 29 Nov 2010 08:01:09 +0000 Christian Urban isarfied some of the high-level proofs
Mon, 29 Nov 2010 05:17:41 +0000 Christian Urban added abs_rename_res lemma
Mon, 29 Nov 2010 05:10:02 +0000 Christian Urban completed proofs in Foo2
Sun, 28 Nov 2010 16:37:34 +0000 Christian Urban completed the strong exhausts rules for Foo2 using general lemmas
Sat, 27 Nov 2010 22:55:29 +0000 Christian Urban disabled the Foo examples, because of heavy work
Fri, 26 Nov 2010 22:43:26 +0000 Christian Urban slightly simplified the Foo2 tests and hint at a general lemma
Fri, 26 Nov 2010 19:03:23 +0000 Christian Urban completely different method fro deriving the exhaust lemma
Fri, 26 Nov 2010 12:17:24 +0900 Cezary Kaliszyk missing freshness assumptions
Thu, 25 Nov 2010 15:06:45 +0900 Cezary Kaliszyk foo2 strong induction
Wed, 24 Nov 2010 17:44:50 +0900 Cezary Kaliszyk foo2 full exhausts
Wed, 24 Nov 2010 16:59:26 +0900 Cezary Kaliszyk Foo2 strong_exhaust for first variable.
Mon, 22 Nov 2010 16:16:25 +0900 Cezary Kaliszyk single rename in let2
Sun, 21 Nov 2010 02:17:19 +0000 Christian Urban added example Foo2.thy
less more (0) tip