nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Feb 2010 10:43:48 +0100] rev 1022

With induct instead of induct_tac, just one induction is sufficient.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Feb 2010 10:20:54 +0100] rev 1021

General alpha_gen_trans for one-variable abstraction.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Feb 2010 09:51:39 +0100] rev 1020

With unfolding Rep/Abs_eqvt no longer needed.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Feb 2010 08:16:34 +0100] rev 1019

Lam2 finished apart from Rep_eqvt.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Feb 2010 20:02:44 +0100] rev 1018

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Feb 2010 16:05:59 +0100] rev 1017

All should be ok now.

Christian Urban <urbanc@in.tum.de> [Mon, 01 Feb 2010 18:57:39 +0100] rev 1016

repaired according to changes in Abs.thy

Christian Urban <urbanc@in.tum.de> [Mon, 01 Feb 2010 18:57:20 +0100] rev 1015

added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case

Christian Urban <urbanc@in.tum.de> [Mon, 01 Feb 2010 16:46:07 +0100] rev 1014

cleaned

Christian Urban <urbanc@in.tum.de> [Mon, 01 Feb 2010 16:23:47 +0100] rev 1013

updated from huffman

nominal2