nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

IntEx.thy

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
2009-12-04	Cezary Kaliszyk	Even more name changes and cleaning	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	More code cleaning and name changes	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	More name changes	file \| diff \| annotate
2009-12-03	Christian Urban	removed quot argument...not all examples work anymore	file \| diff \| annotate
2009-12-03	Christian Urban	merged	file \| diff \| annotate
2009-12-03	Christian Urban	merged	file \| diff \| annotate
2009-12-03	Cezary Kaliszyk	Updated the examples	file \| diff \| annotate
2009-12-03	Christian Urban	merged	file \| diff \| annotate
2009-12-03	Christian Urban	deleted some dead code	file \| diff \| annotate
2009-12-02	Christian Urban	deleted now obsolete argument rty everywhere	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-01	Cezary Kaliszyk	Cleaning 'aps'.	file \| diff \| annotate
2009-11-30	Cezary Kaliszyk	Code cleaning.	file \| diff \| annotate
2009-11-29	Christian Urban	tried to improve the inj_repabs_trm function but left the new part commented out	file \| diff \| annotate
2009-11-29	Cezary Kaliszyk	Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.	file \| diff \| annotate
2009-11-29	Christian Urban	introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]	file \| diff \| annotate
2009-11-28	Christian Urban	removed old inj_repabs_tac; kept only the one with (selective) debugging information	file \| diff \| annotate

less more (0) -100 -50 -30 tip

nominal2

RSS Atom