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/Ex/Lambda.thy

2011-02-23	Cezary Kaliszyk	Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.	file \| diff \| annotate
2011-02-01	Cezary Kaliszyk	Only one of the subgoals is needed	file \| diff \| annotate
2011-01-25	Christian Urban	made eqvt-proof explicit in the function definitions	file \| diff \| annotate
2011-01-19	Christian Urban	added obtain_fresh lemma; tuned Lambda.thy	file \| diff \| annotate
2011-01-19	Christian Urban	ported some of the old proofs to serve as testcases	file \| diff \| annotate
2011-01-19	Christian Urban	defined height as a function that returns an integer	file \| diff \| annotate
2011-01-18	Christian Urban	defined properly substitution	file \| diff \| annotate
2011-01-18	Christian Urban	the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions	file \| diff \| annotate
2011-01-17	Christian Urban	added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)	file \| diff \| annotate
2011-01-17	Christian Urban	added a few examples of functions to Lambda.thy	file \| diff \| annotate
2011-01-17	Christian Urban	removed old testing code from Lambda.thy	file \| diff \| annotate
2011-01-09	Christian Urban	solved subgoals for depth and subst function	file \| diff \| annotate
2011-01-06	Christian Urban	a modified function package where, as a test, True has been injected into the compatibility condictions	file \| diff \| annotate
2011-01-06	Christian Urban	tuned	file \| diff \| annotate
2010-12-31	Christian Urban	changed res keyword to set+ for restrictions; comment by a referee	file \| diff \| annotate

less more (0) -15 tip

nominal2