Re: [isabelle] Specializing types in locales
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:
Your approach with for would work nicely if it did not erase all
mixfix syntax annotations on the parameters.
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