Re: [isabelle] Isabelle2014-RC0 available for testing

Hi Joachim,

Am 09.07.2014 um 20:29 schrieb Joachim Breitner <breitner at>:

> Am Mittwoch, den 09.07.2014, 18:12 +0200 schrieb Jasmin Christian
> Blanchette:
>> Could you give us more context about this error, e.g. a self-contained
>> theory file that we can load to reproduce it (or at least a
>> screenshot)? There have been some changes in the "size" function
>> generation for lists between 2013-2 and 2014-RC0, but we were
>> expecting the changes to be backward-compatible.
> I found that I had to change my theories to refer to size_list instead
> of list_size (but no substantial changes were required)

Fair enough; this is documented in "NEWS" as follows:

  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>

This is merely a cosmetic change. There were also more fundamental changes taking place under the hood.

(Incidentally, I don't quite understand how this connects to the unknown "list.size" constant error you reported, though. Please let us know If this is still an issue.)



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.