nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Quot/Examples/AbsRepTest.thy

2010-01-25	Christian Urban	tuned proofs (mainly in QuotProd)	file \| diff \| annotate
2010-01-24	Christian Urban	test with splits	file \| diff \| annotate
2010-01-12	Cezary Kaliszyk	Finished replacing OO by OOO	file \| diff \| annotate
2010-01-09	Christian Urban	removed obsolete equiv_relation and rnamed new_equiv_relation	file \| diff \| annotate
2010-01-08	Cezary Kaliszyk	Proved concat_empty.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	some cleaning.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	First generalization.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	The working proof of the special case.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	Reduced the proof to two simple but not obvious to prove facts.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	More cleaning and commenting AbsRepTest. Now tests work; just slow.	file \| diff \| annotate
2010-01-07	Cezary Kaliszyk	cleaning in AbsRepTest.	file \| diff \| annotate
2010-01-06	Cezary Kaliszyk	Further in the proof	file \| diff \| annotate
2010-01-05	Cezary Kaliszyk	merge	file \| diff \| annotate
2010-01-05	Cezary Kaliszyk	Trying the proof	file \| diff \| annotate
2010-01-05	Christian Urban	merged	file \| diff \| annotate
2010-01-05	Cezary Kaliszyk	Struggling with composition	file \| diff \| annotate
2010-01-05	Cezary Kaliszyk	Trying to state composition quotient.	file \| diff \| annotate
2010-01-05	Christian Urban	proper handling of error messages (code copy - maybe this can be avoided)	file \| diff \| annotate
2010-01-05	Christian Urban	added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)	file \| diff \| annotate
2010-01-01	Christian Urban	a slight change to abs/rep generation	file \| diff \| annotate
2009-12-26	Christian Urban	corrected wrong [quot_respect] attribute; tuned	file \| diff \| annotate
2009-12-26	Christian Urban	renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy	file \| diff \| annotate
2009-12-26	Christian Urban	generalised absrep function; needs consolidation	file \| diff \| annotate
2009-12-24	Christian Urban	made the quotient_type definition more like typedef; now type variables need to be explicitly given	file \| diff \| annotate
2009-12-23	Christian Urban	used Local_Theory.declaration for storing quotdata	file \| diff \| annotate
2009-12-23	Christian Urban	modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants	file \| diff \| annotate
2009-12-23	Christian Urban	explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions	file \| diff \| annotate
2009-12-23	Christian Urban	corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file	file \| diff \| annotate

less more (0) tip

nominal2

RSS Atom