nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Tue, 12 Jun 2012 01:23:52 +0100] rev 3187

added finfun-type to Nominal

Christian Urban <urbanc@in.tum.de> [Mon, 11 Jun 2012 14:02:57 +0100] rev 3186

added CPS files to test (not all proofs have been completed)

Christian Urban <urbanc@in.tum.de> [Sat, 09 Jun 2012 19:48:19 +0100] rev 3185

added a rule about inequality of freshness between atoms to the simplifier

Christian Urban <urbanc@in.tum.de> [Wed, 06 Jun 2012 14:50:47 +0100] rev 3184

a simproc for simplifying Fresh when there is a sufficiently fresh atom

Christian Urban <urbanc@in.tum.de> [Mon, 04 Jun 2012 21:39:51 +0100] rev 3183

added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often

Christian Urban <urbanc@in.tum.de> [Thu, 31 May 2012 12:01:13 +0100] rev 3182

merged

Christian Urban <urbanc@in.tum.de> [Thu, 31 May 2012 12:01:01 +0100] rev 3181

added to the simplifier nominal_datatype.fresh lemmas

nominal2