[isabelle] Syntaxdefinition in Locales
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Syntaxdefinition in Locales
- From: René Neumann <lists at necoro.eu>
- Date: Wed, 14 Sep 2011 18:45:38 +0200
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:184.108.40.206) Gecko/20110901 Lightning/1.0b3pre Thunderbird/3.1.12
I have the following setting (in Isabelle2011):
definition foo where
"foo a b G = id"
locale spam =
fixes G :: "'a"
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"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and