nominal2: File revisions

QuotMain.thy

2009-12-06	Christian Urban	fixed examples	file \| diff \| annotate
2009-12-06	Christian Urban	working state again	file \| diff \| annotate
2009-12-06	Christian Urban	added a theorem list for equivalence theorems	file \| diff \| annotate
2009-12-06	Christian Urban	updated Isabelle and deleted mono rules	file \| diff \| annotate
2009-12-06	Christian Urban	more tuning of the code	file \| diff \| annotate
2009-12-06	Christian Urban	puting code in separate sections	file \| diff \| annotate
2009-12-06	Cezary Kaliszyk	Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.	file \| diff \| annotate
2009-12-06	Christian Urban	working on lambda_prs with examples; polished code of clean_tac	file \| diff \| annotate
2009-12-06	Christian Urban	renamed lambda_allex_prs	file \| diff \| annotate
2009-12-05	Christian Urban	merged	file \| diff \| annotate
2009-12-05	Christian Urban	added new example for Ints; regularise does not work in all instances	file \| diff \| annotate
2009-12-05	Cezary Kaliszyk	Definitions folded first.	file \| diff \| annotate
2009-12-05	Cezary Kaliszyk	Used symmetric definitions. Moved quotient_rsp to QuotMain.	file \| diff \| annotate
2009-12-05	Christian Urban	moved all_prs and ex_prs out from the conversion into the simplifier	file \| diff \| annotate

nominal2