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/LFex.thy

2010-03-23	Cezary Kaliszyk	Move examples which create more permutations out	file \| diff \| annotate
2010-03-22	Cezary Kaliszyk	Got rid of alpha_bn_rsp_cheat.	file \| diff \| annotate
2010-03-20	Cezary Kaliszyk	Use 'alpha_bn_refl' to get rid of one of the sorrys.	file \| diff \| annotate
2010-03-19	Cezary Kaliszyk	Automatically derive support for datatypes with at-most one binding per constructor.	file \| diff \| annotate
2010-03-19	Cezary Kaliszyk	Use fs typeclass in showing finite support + some cheat cleaning.	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Rename "_property" to ".property"	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Added fv,bn,distinct,perm to the simplifier.	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Rename bound variables + minor cleaning.	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.	file \| diff \| annotate
2010-03-16	Cezary Kaliszyk	FV_bn generated for recursive functions as well, and used in main fv for bindings.	file \| diff \| annotate
2010-03-15	Cezary Kaliszyk	LF works with new alpha...?	file \| diff \| annotate
2010-03-11	Cezary Kaliszyk	Finite_support proof no longer needed in LF.	file \| diff \| annotate
2010-03-08	Cezary Kaliszyk	More fine-grained nominal restriction for debugging.	file \| diff \| annotate
2010-03-05	Cezary Kaliszyk	Ported LF to the parser interface.	file \| diff \| annotate
2010-03-05	Cezary Kaliszyk	Fixed LF for one quantifier over 2 premises.	file \| diff \| annotate

less more (0) -15 tip

nominal2