nominal2: File revisions

QuotMain.thy

2009-12-03	Cezary Kaliszyk	defs used automatically by clean_tac	file \| diff \| annotate
2009-12-03	Cezary Kaliszyk	removing unused code	file \| diff \| annotate
2009-12-03	Christian Urban	deleted some dead code	file \| diff \| annotate
2009-12-03	Cezary Kaliszyk	Included all_prs and ex_prs in the lambda_prs conversion.	file \| diff \| annotate
2009-12-03	Christian Urban	further simplification	file \| diff \| annotate
2009-12-03	Christian Urban	simplified lambda_prs_conv	file \| diff \| annotate
2009-12-02	Christian Urban	deleted now obsolete argument rty everywhere	file \| diff \| annotate
2009-12-02	Christian Urban	deleted tests at the beginning of QuotMain	file \| diff \| annotate
2009-12-02	Cezary Kaliszyk	Experiments with OPTION_map	file \| diff \| annotate
2009-12-02	Cezary Kaliszyk	merge	file \| diff \| annotate
2009-12-02	Cezary Kaliszyk	More experiments with higher order quotients and theorems with non-lifted constants.	file \| diff \| annotate
2009-12-02	Christian Urban	merged	file \| diff \| annotate

nominal2