nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

Quot/Nominal/Abs.thy

2010-02-22	Cezary Kaliszyk	Generalize atom_trans and atom_sym.	file \| diff \| annotate
2010-02-18	Christian Urban	start work with the parser	file \| diff \| annotate
2010-02-12	Cezary Kaliszyk	renamed 'as' to 'is' everywhere.	file \| diff \| annotate
2010-02-11	Cezary Kaliszyk	Main renaming + fixes for new Isabelle in IntEx2.	file \| diff \| annotate
2010-02-09	Christian Urban	merged	file \| diff \| annotate
2010-02-09	Christian Urban	a few more attempts to show the equivalence between old and new way of defining alpha-equivalence	file \| diff \| annotate
2010-02-09	Cezary Kaliszyk	Fixed pattern matching, now the test in Abs works correctly.	file \| diff \| annotate
2010-02-08	Christian Urban	added a test case	file \| diff \| annotate
2010-02-08	Christian Urban	moved some lemmas to Nominal; updated all files	file \| diff \| annotate
2010-02-04	Christian Urban	fixed (permute_eqvt in eqvts makes this simpset always looping)	file \| diff \| annotate
2010-02-03	Christian Urban	fixed proofs in Abs.thy	file \| diff \| annotate
2010-02-03	Cezary Kaliszyk	Minor	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	Disambiguating the syntax.	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	Some equivariance machinery that comes useful in LF.	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	General alpha_gen_trans for one-variable abstraction.	file \| diff \| annotate
2010-02-01	Christian Urban	added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case	file \| diff \| annotate
2010-02-01	Christian Urban	cleaned	file \| diff \| annotate
2010-02-01	Christian Urban	renamed Abst/abst to Abs/abs	file \| diff \| annotate
2010-02-01	Christian Urban	got rid of RAbst type - is now just pairs	file \| diff \| annotate
2010-02-01	Cezary Kaliszyk	Monotonicity of ~~gen, needed for using it in inductive definitions.	file \| diff \| annotate
2010-01-30	Christian Urban	introduced a generic alpha (but not sure whether it is helpful)	file \| diff \| annotate
2010-01-28	Christian Urban	*the supp of a lambda can now be characterised, provided* the notion of free variables coincides with support on lambda terms**	file \| diff \| annotate
2010-01-28	Christian Urban	improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions	file \| diff \| annotate
2010-01-28	Christian Urban	general abstraction operator and complete characterisation of its support and freshness	file \| diff \| annotate
2010-01-28	Christian Urban	attempt of a general abstraction operator	file \| diff \| annotate

less more (0) tip

nominal2

RSS Atom