nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

quotient.ML

2009-11-23	Christian Urban	fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)	file \| diff \| annotate
2009-11-22	Christian Urban	updated to Isabelle 22nd November	file \| diff \| annotate
2009-11-21	Christian Urban	slight tuning	file \| diff \| annotate
2009-11-21	Christian Urban	simplified get_fun so that it uses directly rty and qty, instead of qenv	file \| diff \| annotate
2009-11-20	Christian Urban	started regularize of rtrm/qtrm version; looks quite promising	file \| diff \| annotate
2009-11-19	Christian Urban	updated to new Isabelle	file \| diff \| annotate
2009-11-13	Christian Urban	added some tracing information to all phases of lifting to the function lift_thm	file \| diff \| annotate
2009-11-12	Cezary Kaliszyk	merge of the merge?	file \| diff \| annotate
2009-11-12	Cezary Kaliszyk	merged	file \| diff \| annotate
2009-11-12	Christian Urban	added a FIXME commment	file \| diff \| annotate
2009-11-12	Christian Urban	looking up data in quot_info works now (needs qualified string)	file \| diff \| annotate
2009-11-12	Christian Urban	changed the quotdata to be a symtab table (needs fixing)	file \| diff \| annotate
2009-11-06	Christian Urban	tuned the code in quotient and quotient_def	file \| diff \| annotate
2009-11-05	Christian Urban	*removed typing information from get_fun in quotient_def; potentially* dangerous**	file \| diff \| annotate
2009-11-02	Christian Urban	split quotient.ML into two files	file \| diff \| annotate
2009-11-02	Christian Urban	fixed problem with maps_update	file \| diff \| annotate
2009-11-02	Christian Urban	fixed the problem with types in map	file \| diff \| annotate
2009-10-28	Christian Urban	added infrastructure for defining lifted constants	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-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	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-21	Christian Urban	tuned and attempted to store data about the quotients (does not work yet)	file \| diff \| annotate
2009-10-20	Christian Urban	started to write code for storing data about the quotients	file \| diff \| annotate
2009-10-19	Christian Urban	moved the map-info and fun-info section to quotient.ML	file \| diff \| annotate
2009-10-18	Christian Urban	slight fix and tuning	file \| diff \| annotate
2009-10-17	Christian Urban	the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and	file \| diff \| annotate

less more (0) -30 tip

nominal2

RSS Atom