[isabelle] Strange behavior of binders in locales

Dear Isabelle experts,


I have the following problem when trying to build a locale and changing the concrete syntax of a binder:


Letâs say I have the following definition within locale A:


definition myBinder :: "('a â bool) â bool" (binder "Ab" 10)

  where "myBinder P â True"


Now lets say I have another locale B which is based on A and for which I want to change the syntax of myBinder.

Therefore I add the following in B:


notation myBinder (binder "Bb" 10)


now I get the following error message: âMore than one parse translation for "\<^const>MyTheory.A.myBinder_binderâ


Does someone know how to change the syntax of a binder within a locale?

(By the way it works well for any other mixfix notation)


Many thanks,






Diego Marmsoler

Technische UniversitÃt MÃnchen

FakultÃt fÃr Informatik

Lehrstuhl fÃr Software & Systems Engineering

Zimmer MI 00.11.057

Boltzmannstr. 3

85748 Garching bei MÃnchen

Tel. +49 (0)89 289-17384 

Fax. +49 (0)89 289-17307

 <mailto:diego.marmsoler at tum.de> diego.marmsoler at tum.de

 <http://www4.in.tum.de/~marmsole/> http://www4.in.tum.de/~marmsole/



Attachment: smime.p7s
Description: S/MIME cryptographic signature

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