[isabelle] Syntaxdefinition in Locales



Dear list-members,

I have the following setting (in Isabelle2011):

definition foo where
"foo a b G = id"

locale spam =
   fixes G :: "'a"
begin

  abbreviation f ("_ \<rightarrow>\<star> _" [100,100] 40)
  where	"f a b == foo a b G"

  abbreviation test ("_ \<star> _" [100,100] 40)
  where	"test a b == a > b"

end

locale eggs =
...

sublocale eggs <= spam "some_rather_complex_instantiation"

My problem now is, that my new syntax of f is available in the locale
spam, but not in eggs (after the sublocale proof), while the
abbreviation itself is.

To make things even more tricky: The new syntax defined for 'test' works
just fine in spam and in eggs. It seems like any definition containing G
just kills the syntax interpretation in sublocales.

Is this a bug, a feature or something that is wrong to try in the first
place? My reason is, that I wanted to hide the
'some_rather_complex_instantiation' throughout eggs and its sublocales
whenever I work with foo. (I know, that I could just use the plain
abbreviation without the syntax, but well ... :))

(Btw: Using 'definition' instead of 'abbreviation' does not change
anything).

Thanks,
René





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