[isabelle] Auxiliary context in class target

Hi all,

I am having trouble to use Isabelle's new auxiliary contexts inside a class context, 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 free variable:

*** 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.
I would like to use such a context to emulate the "for" clause of inductive for function defintions, because the induction rule generated by fun is nicer.

Is this just not yet implemented or am I again abusing things here?


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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