blanchet [Thu, 30 Aug 2012 15:57:14 +0200] rev 49031
generate "case_disc" property
blanchet [Thu, 30 Aug 2012 14:52:39 +0200] rev 49030
generate "ctr_sels" theorems
blanchet [Thu, 30 Aug 2012 14:27:26 +0200] rev 49029
generate "disc_exhaust" property
blanchet [Thu, 30 Aug 2012 13:42:05 +0200] rev 49028
generate "disc_distinct" theorems
blanchet [Thu, 30 Aug 2012 11:31:47 +0200] rev 49027
added discriminator theorems
blanchet [Thu, 30 Aug 2012 11:31:20 +0200] rev 49026
adjust example
blanchet [Thu, 30 Aug 2012 09:48:27 +0200] rev 49025
more work on sugar
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49024
updated Java-related error message
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49023
changed order of arguments to "bnf_sugar"
blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49022
define selectors and discriminators