| Fri, 17 Dec 2010 01:01:44 +0000 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 08:42:48 +0000 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 22:09:11 +0000 |
Christian Urban |
created strong_exhausts terms
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 17:07:08 +0000 |
Christian Urban |
first tests about exhaust
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:16:25 +0000 |
Christian Urban |
moved some code into the nominal_library
|
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
|
| Mon, 15 Nov 2010 09:52:29 +0000 |
Christian Urban |
proved that bn functions return a finite set
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 01:10:02 +0000 |
Christian Urban |
fixed bug in fv function where a shallow binder binds lists of names
|
file |
diff |
annotate
|
| Sun, 14 Nov 2010 16:34:47 +0000 |
Christian Urban |
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
|
file |
diff |
annotate
| base
|