Re: [isabelle] Strange behavior of binders in locales

It seems that the behavior can be reproduced even without a hierarchy of locales.
The following reproduces the error message:

locale A

definition test:: "('a â bool) â bool" (binder "+" 10)
  where "test P â True"

notation test (binder "-" 10)


without locale it doesn't produce any error message.



-----UrsprÃngliche Nachricht-----
Von: cl-isabelle-users-bounces at [mailto:cl-isabelle-users-bounces at] Im Auftrag von Diego Marmsoler
Gesendet: Donnerstag, 17. August 2017 17:37
An: cl-isabelle-users at
Betreff: [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> diego.marmsoler at




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

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