nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Quot/QuotMain.thy

2009-12-10	Cezary Kaliszyk	Moved Unused part of locale to Unused QuotMain.	file \| diff \| annotate
2009-12-10	Christian Urban	more tuning	file \| diff \| annotate
2009-12-10	Christian Urban	tuned	file \| diff \| annotate
2009-12-10	Christian Urban	simplified the instantiation of QUOT_TRUE in procedure_tac	file \| diff \| annotate
2009-12-10	Christian Urban	completed previous commit	file \| diff \| annotate
2009-12-10	Christian Urban	deleted DT/NDT diagnostic code	file \| diff \| annotate
2009-12-09	Cezary Kaliszyk	Code cleaning.	file \| diff \| annotate
2009-12-09	Christian Urban	tuned	file \| diff \| annotate
2009-12-09	Cezary Kaliszyk	merge	file \| diff \| annotate
2009-12-09	Cezary Kaliszyk	Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.	file \| diff \| annotate
2009-12-09	Christian Urban	deleted make_inst3	file \| diff \| annotate
2009-12-09	Christian Urban	tuned	file \| diff \| annotate
2009-12-09	Christian Urban	tuned	file \| diff \| annotate
2009-12-09	Christian Urban	moved function and tuned comment	file \| diff \| annotate
2009-12-09	Christian Urban	improved fun_map_conv	file \| diff \| annotate
2009-12-09	Cezary Kaliszyk	Arbitrary number of fun_map_tacs.	file \| diff \| annotate
2009-12-09	Cezary Kaliszyk	Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.	file \| diff \| annotate
2009-12-08	Christian Urban	tuned code	file \| diff \| annotate
2009-12-08	Christian Urban	implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges	file \| diff \| annotate
2009-12-08	Christian Urban	decoupled QuotProd from QuotMain and also started new cleaning strategy	file \| diff \| annotate
2009-12-08	Christian Urban	properly set up the prs_rules	file \| diff \| annotate
2009-12-08	Christian Urban	merged	file \| diff \| annotate
2009-12-08	Christian Urban	added preserve rules to the cleaning_tac	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	merge	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	cleaning.	file \| diff \| annotate
2009-12-08	Christian Urban	chnaged syntax to "lifting theorem"	file \| diff \| annotate
2009-12-08	Christian Urban	changed names of attributes	file \| diff \| annotate
2009-12-08	Christian Urban	merged	file \| diff \| annotate
2009-12-08	Christian Urban	added methods for the lifting_tac and the other tacs	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	make_inst3	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	trans2 replaced with equals_rsp_tac	file \| diff \| annotate
2009-12-08	Cezary Kaliszyk	Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned	file \| diff \| annotate

less more (0) -32 tip

nominal2

RSS Atom