nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 10:44:30 +0100] rev 826

Modifications for new_equiv_rel, part2

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 10:39:08 +0100] rev 825

Modifictaions for new_relation.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 08 Jan 2010 10:08:01 +0100] rev 824

Proved concat_empty.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 16:51:38 +0100] rev 823

Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 16:06:13 +0100] rev 822

some cleaning.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 15:50:22 +0100] rev 821

First generalization.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 14:14:17 +0100] rev 820

The working proof of the special case.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 10:55:20 +0100] rev 819

Reduced the proof to two simple but not obvious to prove facts.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 10:13:15 +0100] rev 818

More cleaning and commenting AbsRepTest. Now tests work; just slow.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 07 Jan 2010 09:55:42 +0100] rev 817

cleaning in AbsRepTest.

nominal2