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 |