nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

QuotMain.thy

2009-10-28	Christian Urban	added infrastructure for defining lifted constants	file \| diff \| annotate
2009-10-28	Cezary Kaliszyk	First experiments with Lambda	file \| diff \| annotate
2009-10-28	Cezary Kaliszyk	Proof of append_rsp	file \| diff \| annotate
2009-10-28	Christian Urban	merged	file \| diff \| annotate
2009-10-28	Christian Urban	added a function for matching types	file \| diff \| annotate
2009-10-27	Cezary Kaliszyk	Simplfied interface to repabs_injection.	file \| diff \| annotate
2009-10-27	Cezary Kaliszyk	map_append lifted automatically.	file \| diff \| annotate
2009-10-27	Cezary Kaliszyk	Merged	file \| diff \| annotate
2009-10-27	Cezary Kaliszyk	Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.	file \| diff \| annotate
2009-10-27	Christian Urban	tuned	file \| diff \| annotate
2009-10-27	Christian Urban	added equiv-thm to the quot_info	file \| diff \| annotate
2009-10-27	Christian Urban	made quotients compatiple with Nominal; updated keyword file	file \| diff \| annotate
2009-10-27	Cezary Kaliszyk	Completely cleaned Int.	file \| diff \| annotate
2009-10-27	Cezary Kaliszyk	Further reordering in Int code.	file \| diff \| annotate
2009-10-26	Christian Urban	merged	file \| diff \| annotate
2009-10-26	Cezary Kaliszyk	Symmetry of integer addition	file \| diff \| annotate
2009-10-26	Cezary Kaliszyk	Finished the code for adding lower defs, and more things moved to QuotMain	file \| diff \| annotate
2009-10-26	Cezary Kaliszyk	Cleaning and fixing.	file \| diff \| annotate
2009-10-25	Christian Urban	added code for declaring map-functions	file \| diff \| annotate
2009-10-24	Christian Urban	added data-storage about the quotients	file \| diff \| annotate
2009-10-24	Christian Urban	changed the definitions of liftet constants to use fun_maps	file \| diff \| annotate
2009-10-24	Christian Urban	moved the map_funs setup into QuotMain	file \| diff \| annotate
2009-10-24	cek	Undid wrong merge	file \| diff \| annotate
2009-10-24	cek	Cleaning the mess	file \| diff \| annotate
2009-10-23	Christian Urban	fixed problem with incorrect ABS/REP name	file \| diff \| annotate
2009-10-23	Cezary Kaliszyk	Split Finite Set example into separate file	file \| diff \| annotate
2009-10-23	Cezary Kaliszyk	eqsubst_tac	file \| diff \| annotate
2009-10-23	Cezary Kaliszyk	Trying to get a simpler lemma with the whole infrastructure	file \| diff \| annotate

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

nominal2

RSS Atom