nominal2: File revisions

Nominal/Parser.thy

2010-03-23	Cezary Kaliszyk	Move examples which create more permutations out	file \| diff \| annotate
2010-03-22	Cezary Kaliszyk	equivp_cheat can be removed for all one-permutation examples.	file \| diff \| annotate
2010-03-22	Cezary Kaliszyk	Got rid of alpha_bn_rsp_cheat.	file \| diff \| annotate
2010-03-22	Cezary Kaliszyk	fv_rsp proved automatically.	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-20	Cezary Kaliszyk	Prove reflp for all relations.	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	Remove atom_decl from the parser.	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	case names also for _induct	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Case_Names for _inducts. Does not work for _induct yet.	file \| diff \| annotate
2010-03-18	Cezary Kaliszyk	Added fv,bn,distinct,perm to the simplifier.	file \| diff \| annotate

nominal2