nominal2: File revisions

Nominal-General/Nominal2_Eqvt.thy

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	file \| diff \| annotate
Wed, 05 May 2010 10:24:54 +0100	Christian Urban	solved the problem with equivariance by first eta-normalising the goal	file \| diff \| annotate
Sun, 02 May 2010 16:00:52 +0100	Christian Urban	removed duplicate eqvt attribute	file \| diff \| annotate
Fri, 30 Apr 2010 14:21:18 +0100	Christian Urban	added eqvt-lemmas for Bex, Ball and Union	file \| diff \| annotate
Fri, 30 Apr 2010 10:09:45 +0100	Christian Urban	reorganised eqvt-file (now uses perm_simp already)	file \| diff \| annotate
Wed, 28 Apr 2010 08:22:20 +0200	Christian Urban	simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base	file \| diff \| annotate
Tue, 27 Apr 2010 22:21:16 +0200	Christian Urban	moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base	file \| diff \| annotate

nominal2