nominal2: Shortlog

Mercurial Mercurial > hg > nominal2 / shortlog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -16 +16 +100 +300 tip

2011-01-17	Christian Urban	removed old testing code from Lambda.thy	changeset \| files
2011-01-17	Christian Urban	moved high level code from LamTest into the main libraries.	changeset \| files
2011-01-17	Christian Urban	eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation	changeset \| files
2011-01-15	Christian Urban	subst also works now	changeset \| files
2011-01-15	Christian Urban	nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions	changeset \| files
2011-01-14	Christian Urban	strengthened renaming lemmas	changeset \| files
2011-01-13	Christian Urban	added eqvt_lemmas for subset and psubset	changeset \| files
2011-01-10	Christian Urban	a few lemmas about freshness for at and at_base	changeset \| files
2011-01-10	Christian Urban	added a property about finite support in the presense of eqvt_at	changeset \| files
2011-01-09	Christian Urban	instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis	changeset \| files
2011-01-09	Christian Urban	solved subgoals for depth and subst function	changeset \| files
2011-01-09	Christian Urban	added eqvt_at premises in function definition - however not proved at the moment	changeset \| files
2011-01-07	Christian Urban	added one further lemma about equivariance of THE_default	changeset \| files
2011-01-07	Christian Urban	equivariance of THE_default under the uniqueness assumption	changeset \| files
2011-01-07	Christian Urban	derived equivariance for the function graph and function relation	changeset \| files
2011-01-06	Christian Urban	a modified function package where, as a test, True has been injected into the compatibility condictions	changeset \| files

(0) -1000 -300 -100 -16 +16 +100 +300 tip

nominal2