*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Porting trouble: Interpretation of locale semiring_1*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Wed, 22 Apr 2009 18:55:01 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Quoting Peter Lammich <peter.lammich at uni-muenster.de>:

I'm currently converting theories from 2008 -> 2009: ... *** Partially applied constant on left hand side of equation *** "semiring_1.of_nat {[]} {} op \<union> ?n \<equiv> semiring_1.of_nat_aux (\<lambda>i. i \<union> {[]}) ?n {}" *** At command "done". I do not know what this error message means, nor can I find any documentation. In Isabelle2008, the proof worked well.

This error is generated by the code generator (while processing the interpreted lemmas). It is apparently unable to deal with the equation generated by the interpretation.

Clemens

**Follow-Ups**:

- Previous by Date: Re: [isabelle] Isabelle2009: Where's the [!] after lemmas that are not proven ?
- Next by Date: Re: [isabelle] Defines in locales in Isabelle 2009
- Previous by Thread: Re: [isabelle] Isabelle2009: Where's the [!] after lemmas that are not proven ?
- Next by Thread: Re: [isabelle] Porting trouble: Interpretation of locale semiring_1
- Cl-isabelle-users April 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list