nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Nominal/Ex/Lambda.thy

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
2010-12-28	Christian Urban	automated all strong induction lemmas	file \| diff \| annotate
2010-12-22	Christian Urban	properly exported strong exhaust theorem; cleaned up some examples	file \| diff \| annotate
2010-11-10	Christian Urban	adapted to changes by Florian on the quotient package and removed local fix for function package	file \| diff \| annotate
2010-09-29	Christian Urban	simplified exhaust proofs	file \| diff \| annotate
2010-09-29	Christian Urban	test with induct_schema for simpler strong_ind proofs	file \| diff \| annotate
2010-08-29	Christian Urban	renamed NewParser to Nominal2	file \| diff \| annotate
2010-08-27	Christian Urban	make copies of the "old" files	file \| diff \| annotate
2010-08-26	Christian Urban	"isabelle make test" makes all major examples....they work up to supp theorems (excluding)	file \| diff \| annotate
2010-08-25	Christian Urban	cleaned up (almost completely) the examples	file \| diff \| annotate
2010-08-25	Christian Urban	automatic lifting	file \| diff \| annotate
2010-08-25	Christian Urban	now every lemma lifts (even with type variables)	file \| diff \| annotate
2010-08-25	Christian Urban	can now deal with type variables in nominal datatype definitions	file \| diff \| annotate
2010-08-21	Christian Urban	nominal_datatypes with type variables do not work	file \| diff \| annotate
2010-08-21	Christian Urban	changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default	file \| diff \| annotate
2010-06-07	Christian Urban	work on transitivity proof	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Match_Lam defined on Quotient Level.	file \| diff \| annotate

less more (0) -50 -24 tip

nominal2

RSS Atom