IntEx.thy
2009-12-05 Christian Urban added new example for Ints; regularise does not work in all instances
2009-12-05 Cezary Kaliszyk Proved foldl_rsp and ho_map_rsp
2009-12-05 Christian Urban moved all_prs and ex_prs out from the conversion into the simplifier
2009-12-05 Cezary Kaliszyk Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban simpler version of clean_tac
2009-12-05 Cezary Kaliszyk Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
2009-12-05 Cezary Kaliszyk Solutions to IntEx tests.
2009-12-05 Christian Urban made some slight simplifications to the examples
2009-12-05 Christian Urban added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
2009-12-04 Christian Urban not yet quite functional treatment of constants
2009-12-04 Cezary Kaliszyk More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
less more (0) -100 -14 tip