Tue, 28 Dec 2010 19:51:25 +0000 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
Thu, 23 Dec 2010 01:05:05 +0000 |
Christian Urban |
test with strong inductions
|
file |
diff |
annotate
|
Thu, 23 Dec 2010 00:46:06 +0000 |
Christian Urban |
moved all strong_exhaust code to nominal_dt_quot; tuned examples
|
file |
diff |
annotate
|
Tue, 07 Dec 2010 14:27:39 +0000 |
Christian Urban |
automated permute_bn theorems
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 16:35:42 +0000 |
Christian Urban |
automated alpha_perm_bn theorems
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Sun, 28 Nov 2010 16:37:34 +0000 |
Christian Urban |
completed the strong exhausts rules for Foo2 using general lemmas
|
file |
diff |
annotate
|
Sat, 27 Nov 2010 22:55:29 +0000 |
Christian Urban |
disabled the Foo examples, because of heavy work
|
file |
diff |
annotate
|
Sun, 21 Nov 2010 02:17:19 +0000 |
Christian Urban |
added example Foo2.thy
|
file |
diff |
annotate
|
Mon, 15 Nov 2010 20:54:01 +0000 |
Christian Urban |
tuned example
|
file |
diff |
annotate
|
Mon, 15 Nov 2010 09:52:29 +0000 |
Christian Urban |
proved that bn functions return a finite set
|
file |
diff |
annotate
|
Sun, 14 Nov 2010 10:02:30 +0000 |
Christian Urban |
tuned example
|
file |
diff |
annotate
|
Sat, 13 Nov 2010 22:23:26 +0000 |
Christian Urban |
lifted permute_bn constants
|
file |
diff |
annotate
|
Sat, 13 Nov 2010 10:25:03 +0000 |
Christian Urban |
respectfulness for permute_bn functions
|
file |
diff |
annotate
|
Fri, 12 Nov 2010 01:20:53 +0000 |
Christian Urban |
automated permute_bn functions (raw ones first)
|
file |
diff |
annotate
|
Wed, 10 Nov 2010 13:46:21 +0000 |
Christian Urban |
adapted to changes by Florian on the quotient package and removed local fix for function package
|
file |
diff |
annotate
|
Wed, 29 Sep 2010 16:49:13 -0400 |
Christian Urban |
simplified exhaust proofs
|
file |
diff |
annotate
|
Wed, 29 Sep 2010 09:47:26 -0400 |
Christian Urban |
worked example Foo1 with induct_schema
|
file |
diff |
annotate
|
Tue, 28 Sep 2010 05:56:11 -0400 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|