nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Tue, 05 Jul 2011 15:01:10 +0200] rev 2947

added another example which seems difficult to define

Christian Urban <urbanc@in.tum.de> [Tue, 05 Jul 2011 15:00:41 +0200] rev 2946

added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.

Christian Urban <urbanc@in.tum.de> [Tue, 05 Jul 2011 04:23:33 +0200] rev 2945

merged

Christian Urban <urbanc@in.tum.de> [Tue, 05 Jul 2011 04:19:02 +0200] rev 2944

all FCB lemmas

Christian Urban <urbanc@in.tum.de> [Tue, 05 Jul 2011 04:18:45 +0200] rev 2943

exported various FCB-lemmas to a separate file

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jul 2011 10:13:34 +0900] rev 2942

Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 05 Jul 2011 09:28:16 +0900] rev 2941

Define a version of aux only for same binders. Completeness is fine.

nominal2