src/HOL/Nominal/Examples/CR_Takahashi.thy
Fri, 04 Jan 2008 09:34:11 +0100 urbanc adapted to new inversion rules
Wed, 11 Jul 2007 11:36:06 +0200 berghofe Renamed inductive2 to inductive.
Thu, 31 May 2007 15:23:35 +0200 urbanc tuned the proof
Tue, 08 May 2007 01:40:30 +0200 urbanc polished some proofs
Fri, 04 May 2007 04:17:00 +0200 urbanc polished all proofs and made the theory "self-contained"
Wed, 02 May 2007 01:42:23 +0200 urbanc tuned some proofs and changed variable names in some definitions of Nominal.thy
Fri, 27 Apr 2007 14:21:23 +0200 urbanc alternative and much simpler proof for Church-Rosser of Beta-Reduction
less more (0) tip