Re: [isabelle] Specializing types in locales
Your approach with for would work nicely if it did not erase all
mixfix syntax annotations on the parameters.
Sorry, I had misread your message.
The syntax of a *parameter* is either given in a fixes element or a
for clause. If no syntax is specified, this means that no syntax is
requested. This is so even in a for clause, because there needs to be
a mechanism to get rid of unwanted syntax when extending a locale.
While replying I though of the syntax of a *constant* (as introduced
by a definition statement). Those are preserved under changes of the
Yes, it still does, at least with the Isabelle versions I tested:
Isabelle repository version 43916ac560a4 and Isabelle 2009-2. Here
is a small example:
locale A =
fixes a :: "'b => 'c" ("%_%")
locale B = A begin
term "%undefined%" -- "works fine"
locale C =
for a :: "'b => 'c"
term "%undefined%" -- "Gives inner syntax error at %"
This archive was generated by a fusion of
Pipermail (Mailman edition) and