nominal2: File revisions

IntEx.thy

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	Proved foldl_rsp and ho_map_rsp	file \| diff \| annotate
2009-12-05	Christian Urban	moved all_prs and ex_prs out from the conversion into the simplifier	file \| diff \| annotate
2009-12-05	Cezary Kaliszyk	Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.	file \| diff \| annotate
2009-12-05	Christian Urban	merged	file \| diff \| annotate
2009-12-05	Christian Urban	merged	file \| diff \| annotate
2009-12-05	Christian Urban	merged	file \| diff \| annotate
2009-12-05	Christian Urban	simpler version of clean_tac	file \| diff \| annotate
2009-12-05	Cezary Kaliszyk	Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.	file \| diff \| annotate
2009-12-05	Cezary Kaliszyk	Solutions to IntEx tests.	file \| diff \| annotate
2009-12-05	Christian Urban	made some slight simplifications to the examples	file \| diff \| annotate
2009-12-05	Christian Urban	added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet	file \| diff \| annotate
2009-12-04	Christian Urban	not yet quite functional treatment of constants	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList	file \| diff \| annotate

nominal2