Re: [isabelle] Specializing types in locales



Hi Clemens,

Your approach with for would work nicely if it did not erase all mixfix syntax annotations on the parameters.

Does it?
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"
end

locale C =
  A a
  for a :: "'b => 'c"
begin
term "%undefined%" -- "Gives inner syntax error at %"
end

Andreas





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