nominal2: File revisions

Nominal/Ex/Classical.thy

Wed, 12 May 2010 16:32:44 +0200	Cezary Kaliszyk	Use equivariance instead of alpha_eqvt	file \| diff \| annotate
Tue, 11 May 2010 18:20:25 +0200	Cezary Kaliszyk	Include raw permutation definitions in eqvt	file \| diff \| annotate
Tue, 11 May 2010 17:16:57 +0200	Cezary Kaliszyk	Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'	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
Mon, 03 May 2010 15:47:30 +0200	Cezary Kaliszyk	Added cheats to classical	file \| diff \| annotate
Sun, 02 May 2010 14:06:26 +0100	Christian Urban	attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)	file \| diff \| annotate
Fri, 16 Apr 2010 16:29:11 +0200	Christian Urban	automatic proofs for equivariance of alphas	file \| diff \| annotate
Thu, 08 Apr 2010 11:40:13 +0200	Christian Urban	properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)	file \| diff \| annotate

nominal2