Re: [isabelle] Isabelle2014-RC0 available for testing



Dear Jasmin,

Am Mittwoch, den 09.07.2014, 18:12 +0200 schrieb Jasmin Christian
Blanchette:
> Am 08.07.2014 um 16:46 schrieb Joachim Breitner <breitner at kit.edu>:
> > * I just observed an error message in the output window:
> >        Undefined constant: "list.size"⌂
> 
> 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)

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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