nominal2: File revisions

Nominal/Ex/Classical.thy

Tue, 05 Jul 2011 15:01:10 +0200	Christian Urban	added another example which seems difficult to define	file \| diff \| annotate
Tue, 05 Jul 2011 04:18:45 +0200	Christian Urban	exported various FCB-lemmas to a separate file	file \| diff \| annotate
Wed, 29 Jun 2011 19:21:26 +0100	Christian Urban	moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through	file \| diff \| annotate
Tue, 28 Jun 2011 12:36:34 +0900	Cezary Kaliszyk	Experiments with res	file \| diff \| annotate
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

nominal2