nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Feb 2010 18:09:20 +0100] rev 1065

The automatic lifting translation function, still with dummy types, but works everywhere in the LF example.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Feb 2010 17:58:23 +0100] rev 1064

Quotdata_dest needed for lifting theorem translation.

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 17:39:04 +0100] rev 1063

fixed (permute_eqvt in eqvts makes this simpset always looping)

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 15:19:24 +0100] rev 1062

rollback of the test

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 15:16:34 +0100] rev 1061

linked versions - instead of copies

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 14:55:52 +0100] rev 1060

merged

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 14:55:21 +0100] rev 1059

restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Feb 2010 18:28:50 +0100] rev 1058

More let-rec experiments

nominal2