Nominal-General/Nominal2_Eqvt.thy
Thu, 03 Jun 2010 15:02:52 +0200 Christian Urban added uminus_eqvt
Thu, 27 May 2010 18:30:26 +0200 Christian Urban fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
Thu, 13 May 2010 18:19:48 +0100 Christian Urban added flip_eqvt and swap_eqvt to the equivariance lists
Sun, 09 May 2010 11:37:19 +0100 Christian Urban added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Wed, 05 May 2010 10:24:54 +0100 Christian Urban solved the problem with equivariance by first eta-normalising the goal
Sun, 02 May 2010 16:00:52 +0100 Christian Urban removed duplicate eqvt attribute
less more (0) -10 -6 tip