nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 13:37:07 +0200] rev 86

Regularizing HOL all.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:38:35 +0200] rev 85

":" is used for being in a set, "IN" means something else...

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:03:55 +0200] rev 84

First (untested) version of regularize for abstractions.

Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 09:26:19 +0200] rev 83

restored old version

Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 00:02:22 +0200] rev 82

tuned

Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:39:14 +0200] rev 81

slightly modified the parser

Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:16:20 +0200] rev 80

deleted diagnostic code

Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:06:14 +0200] rev 79

added quotient command (you need to update isar-keywords-prove.el)

Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 22:44:16 +0200] rev 78

added new keyword

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 16:31:29 +0200] rev 77

Bounded quantifier

nominal2