nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:33:04 +0100] rev 445

renamed r_mk_comb_tac to inj_repabs_tac

Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:15:05 +0100] rev 444

tuning

Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:03:01 +0100] rev 443

tuned comments

Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 13:54:48 +0100] rev 442

renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 08:46:24 +0100] rev 441

Manually finished LF induction.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 08:04:23 +0100] rev 440

Moved fast instantiation to QuotMain

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 07:44:17 +0100] rev 439

LFex proof a bit further.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 06:15:06 +0100] rev 438

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 06:14:50 +0100] rev 437

Looking at repabs proof in LF.

Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 05:53:31 +0100] rev 436

further proper merge

nominal2