nominal2: File revisions

Nominal/Ex/Classical.thy

Tue, 28 Jun 2011 00:48:57 +0100	Christian Urban	proved the fcb also for sets (no restriction yet)	file \| diff \| annotate
Mon, 27 Jun 2011 22:51:42 +0100	Christian Urban	streamlined the fcb-proof and made fcb1 a special case of fcb	file \| diff \| annotate
Mon, 27 Jun 2011 19:22:10 +0100	Christian Urban	completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier)	file \| diff \| annotate
Mon, 27 Jun 2011 19:15:18 +0100	Christian Urban	fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.	file \| diff \| annotate
Mon, 27 Jun 2011 04:01:55 +0900	Cezary Kaliszyk	equality of lst_binder and a few helper lemmas	file \| diff \| annotate
Sun, 26 Jun 2011 21:42:07 +0100	Christian Urban	only one of the fcb precondistions are needed (probably the same with the perm-conditions)	file \| diff \| annotate
Sun, 26 Jun 2011 17:55:22 +0100	Christian Urban	another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy	file \| diff \| annotate
Sat, 25 Jun 2011 22:51:43 +0100	Christian Urban	did all cases, except the multiple binder case	file \| diff \| annotate

nominal2