[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

 

 

--

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.