nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

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

Nominal/nominal_function_core.ML

2011-11-03	Christian Urban	updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package	file \| diff \| annotate
2011-08-19	Cezary Kaliszyk	Update to new Isabelle	file \| diff \| annotate
2011-07-19	Christian Urban	generated the partial eqvt-theorem for functions	file \| diff \| annotate
2011-07-18	Christian Urban	added a flag (eqvt) to termination proofs arising fron nominal_primrecs	file \| diff \| annotate
2011-06-22	Christian Urban	some rudimentary infrastructure for storing data about nominal datatypes	file \| diff \| annotate
2011-06-16	Christian Urban	added eqvt_at and invariant for boths sides of the equations	file \| diff \| annotate
2011-06-14	Christian Urban	fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough	file \| diff \| annotate
2011-06-07	Christian Urban	cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file	file \| diff \| annotate
2011-06-07	Christian Urban	fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant	file \| diff \| annotate
2011-06-05	Christian Urban	added an option for an invariant (at the moment only a stub)	file \| diff \| annotate
2011-06-01	Christian Urban	hopefully final fix for ho-functions	file \| diff \| annotate
2011-06-01	Christian Urban	first test to fix the problem with free variables	file \| diff \| annotate
2011-05-31	Christian Urban	fixed the problem with cps-like functions	file \| diff \| annotate
2011-05-30	Christian Urban	tuned last commit	file \| diff \| annotate
2011-05-30	Christian Urban	functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition	file \| diff \| annotate

less more (0) -15 tip

nominal2