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"

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


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