*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Code generator "eq" instances*From*: John Matthews <matthews at galois.com>*Date*: Wed, 9 Jun 2010 22:47:42 -0700

theory Silly imports Main begin datatype silly = Silly int instantiation silly :: eq begin fun "eq_class.eq" where "eq (Silly n) (Silly m) = (m - n = 0)" instance .. end The "fun" command returns the error *** Bad name binding "eq_class.eq" *** At command "fun". Am I, in fact, doing something silly here? Thanks, -john

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Code generator "eq" instances***From:*Florian Haftmann

- Previous by Date: [isabelle] Proving a simple lemma
- Next by Date: Re: [isabelle] Code generator "eq" instances
- Previous by Thread: Re: [isabelle] Proving a simple lemma
- Next by Thread: Re: [isabelle] Code generator "eq" instances
- Cl-isabelle-users June 2010 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