Re: [isabelle] Isabelle2014-RC0 available for testing



Hi Joachim,

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

> 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" ~>
    "case_prod").
    INCOMPATIBILITY.

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.)

Cheers,

Jasmin





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