*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Auxiliary context in class target*From*: Makarius <makarius at sketis.net>*Date*: Thu, 31 May 2012 10:33:48 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FC5DA75.7030305@kit.edu>*References*: <4FC5DA75.7030305@kit.edu>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 30 May 2012, Andreas Lochbihler wrote:

I am having trouble to use Isabelle's new auxiliary contexts inside a classcontext, as in the following example:context ord begin context fixes x :: 'a begin definition bar where "bar = x"The definition is rejected because x is erroneously identified as a freevariable:*** Extra variables on rhs: "x" *** The error(s) above occurred in definition "ord_class.ord_class.bar_dict": *** "bar == ord.bar x" *** At command "definition"The same error occurs when I use fun with a more complicated function. Iwould like to use such a context to emulate the "for" clause ofinductive for function defintions, because the induction rule generatedby fun is nicer.

Makarius

**References**:**[isabelle] Auxiliary context in class target***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Automation is awesome; one bibliography leads to another
- Next by Date: Re: [isabelle] Automation is awesome; one bibliography leads to another
- Previous by Thread: [isabelle] Auxiliary context in class target
- Next by Thread: [isabelle] inquiry
- Cl-isabelle-users May 2012 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