nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Quot/Examples/AbsRepTest.thy

2010-02-15	Christian Urban	tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy	file \| diff \| annotate
2010-02-11	Cezary Kaliszyk	Main renaming + fixes for new Isabelle in IntEx2.	file \| diff \| annotate
2010-02-09	Cezary Kaliszyk	More indentation, names and todo cleaning in the quotient package	file \| diff \| annotate
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

less more (0) -24 tip

nominal2

RSS Atom