nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -16 tip

IntEx.thy

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
2009-11-28	Christian Urban	renamed r_mk_comb_tac to inj_repabs_tac	file \| diff \| annotate
2009-11-28	Cezary Kaliszyk	Merged and tested that all works.	file \| diff \| annotate
2009-11-28	Cezary Kaliszyk	Finished and tested the new regularize	file \| diff \| annotate
2009-11-28	Christian Urban	fixed examples in IntEx and FSet	file \| diff \| annotate
2009-11-28	Christian Urban	fixed previous commit	file \| diff \| annotate
2009-11-28	Christian Urban	annotated a proof with all steps and simplified LAMBDA_RES_TAC	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Simplifying arguments; got rid of trans2_thm.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Removing arguments of tactics: absrep, rel_refl, reps_same are computed.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Minor cleaning	file \| diff \| annotate
2009-11-27	Christian Urban	introduced a separate lemma for id_simps	file \| diff \| annotate
2009-11-27	Christian Urban	deleted obsolete qenv code	file \| diff \| annotate

less more (0) -16 tip

nominal2