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

2010-03-22	Cezary Kaliszyk	Got rid of alpha_bn_rsp_cheat.	file \| diff \| annotate
2010-03-22	Cezary Kaliszyk	Strong induction for Type Schemes.	file \| diff \| annotate
2010-03-20	Cezary Kaliszyk	Size experiments.	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-19	Cezary Kaliszyk	TySch strong induction looks ok.	file \| diff \| annotate
2010-03-19	Cezary Kaliszyk	Working on TySch strong induction.	file \| diff \| annotate
2010-03-19	Cezary Kaliszyk	Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...	file \| diff \| annotate
2010-03-19	Cezary Kaliszyk	The nominal infrastructure for fset. 'fs' missing, but not needed so far.	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	support of fset_to_set, support of fmap_atom.	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.	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

less more (0) -15 tip

nominal2