nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip

Quot/quotient_typ.ML

2010-01-02	Christian Urban	added a warning to the quotient_type definition, if a map function is missing	file \| diff \| annotate
2010-01-01	Christian Urban	tuned	file \| diff \| annotate
2010-01-01	Christian Urban	some slight tuning	file \| diff \| annotate
2009-12-31	Christian Urban	renamed transfer to transform (Markus)	file \| diff \| annotate
2009-12-26	Christian Urban	tuned	file \| diff \| annotate
2009-12-26	Christian Urban	generalised absrep function; needs consolidation	file \| diff \| annotate
2009-12-24	Christian Urban	tuned	file \| diff \| annotate
2009-12-24	Christian Urban	added sanity checks for quotient_type	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	cleaed a bit function mk_typedef_main	file \| diff \| annotate
2009-12-23	Christian Urban	renamed QUOT_TYPE to Quot_Type	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-19	Christian Urban	renamed "quotient" command to "quotient_type"; needs new keyword file to be installed	file \| diff \| annotate
2009-12-19	Christian Urban	avoided global "open"s - replaced by local "open"s	file \| diff \| annotate
2009-12-19	Christian Urban	various tunings; map_lookup now raises an exception; addition to FIXME-TODO	file \| diff \| annotate
2009-12-12	Christian Urban	renamed quotient.ML to quotient_typ.ML	file \| diff \| annotate \| base

less more (0) tip

nominal2