Re: [isabelle] Specializing types in locales



Hi Andreas,

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

Does it?  I had hoped this was fixed with

changeset:   32985:6c273b0e0e26
user:        ballarin
date:        Mon Nov 02 21:27:26 2009 +0100
summary: Relax on type agreement with original context when applying term sy
ntax.

which should keep the syntax provided only the type of the parameter is changed.

Clemens






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