Quot/Nominal/Nominal2_Eqvt.thy
Wed, 03 Feb 2010 12:06:10 +0100 Christian Urban added a first eqvt_tac which pushes permutations inside terms
Tue, 26 Jan 2010 20:07:50 +0100 Christian Urban added an LamEx example together with the new nominal infrastructure
less more (0) tip