| Mon, 15 Dec 2008 07:41:07 +0000 |
Christian Urban |
tuned some proofs
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 13:24:45 +0100 |
berghofe |
Modified nominal_primrec to make it work with local theories, unified syntax
|
file |
diff |
annotate
|
| Thu, 22 May 2008 16:34:41 +0200 |
urbanc |
made the naming of the induction principles consistent: weak_induct is
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 11:08:18 +0100 |
urbanc |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 15:19:17 +0100 |
urbanc |
tuned proofs and comments
|
file |
diff |
annotate
|
| Tue, 08 Jan 2008 23:11:08 +0100 |
urbanc |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2008 09:34:11 +0100 |
urbanc |
adapted to new inversion rules
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:36:06 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| Thu, 31 May 2007 15:23:35 +0200 |
urbanc |
tuned the proof
|
file |
diff |
annotate
|
| Tue, 08 May 2007 01:40:30 +0200 |
urbanc |
polished some proofs
|
file |
diff |
annotate
|
| Fri, 04 May 2007 04:17:00 +0200 |
urbanc |
polished all proofs and made the theory "self-contained"
|
file |
diff |
annotate
|
| Wed, 02 May 2007 01:42:23 +0200 |
urbanc |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
file |
diff |
annotate
|
| Fri, 27 Apr 2007 14:21:23 +0200 |
urbanc |
alternative and much simpler proof for Church-Rosser of Beta-Reduction
|
file |
diff |
annotate
|