nominal2: File revisions

FSet.thy

2009-11-04	Cezary Kaliszyk	Experiments in Int	file \| diff \| annotate
2009-11-04	Christian Urban	simplified the quotient_def code	file \| diff \| annotate
2009-11-04	Cezary Kaliszyk	Lifting 'fold1.simps(2)' and some cleaning.	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	merge	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	applic_prs	file \| diff \| annotate
2009-11-03	Christian Urban	simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated	file \| diff \| annotate
2009-11-03	Cezary Kaliszyk	Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP	file \| diff \| annotate
2009-11-02	Cezary Kaliszyk	Fixes after optimization and preparing for a general FORALL_PRS	file \| diff \| annotate
2009-11-02	Cezary Kaliszyk	Map does not fully work yet.	file \| diff \| annotate
2009-11-02	Cezary Kaliszyk	Fixed quotdata_lookup.	file \| diff \| annotate
2009-11-02	Christian Urban	merged	file \| diff \| annotate
2009-11-02	Christian Urban	fixed the problem with types in map	file \| diff \| annotate
2009-10-31	Cezary Kaliszyk	Automatic computation of application preservation and manually finished "alpha.induct". Slow...	file \| diff \| annotate
2009-10-30	Cezary Kaliszyk	Regularize for equalities and a better tactic. "alpha.cases" now lifts.	file \| diff \| annotate
2009-10-30	Cezary Kaliszyk	Regularization	file \| diff \| annotate

nominal2