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

2010-03-15	Cezary Kaliszyk	build_eqvts works with recursive case if proper induction rule is used.	file \| diff \| annotate
2010-03-13	Christian Urban	started supp-fv proofs (is going to work)	file \| diff \| annotate
2010-03-12	Cezary Kaliszyk	Even with pattern simplified to a single clause, the supp equation doesn't seem true.	file \| diff \| annotate
2010-03-12	Cezary Kaliszyk	Still don't know how to prove supp=fv for simplest Let...	file \| diff \| annotate
2010-03-11	Cezary Kaliszyk	Finite_support proof no longer needed in LF.	file \| diff \| annotate
2010-03-11	Cezary Kaliszyk	Show that the new types are in finite support typeclass.	file \| diff \| annotate
2010-03-11	Cezary Kaliszyk	Fixes for term1 for new alpha. Still not able to show support equations.	file \| diff \| annotate
2010-03-10	Cezary Kaliszyk	alpha_eqvt for recursive term1.	file \| diff \| annotate
2010-03-08	Cezary Kaliszyk	Undo effects of simp.	file \| diff \| annotate
2010-03-05	Cezary Kaliszyk	Still unable to show supp=fv for let with one existential.	file \| diff \| annotate
2010-03-05	Cezary Kaliszyk	Not much progress about the single existential let case.	file \| diff \| annotate
2010-03-05	Cezary Kaliszyk	Trying to fix the proofs for the single existential... So far failed.	file \| diff \| annotate
2010-03-02	Cezary Kaliszyk	Fixed eqvt code.	file \| diff \| annotate
2010-03-01	Cezary Kaliszyk	Trying to prove equivariance.	file \| diff \| annotate
2010-02-26	Christian Urban	generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"	file \| diff \| annotate

less more (0) -15 tip

nominal2