[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
makarius at sketis.net
Wed Feb 9 16:12:28 CET 2011
On Wed, 9 Feb 2011, Alexander Krauss wrote:
> I don't think that anybody wants to say (or imply) anything like that.
> As I understood it, this particular point ("Why do nonzero indexnames
> show up in this situation, and shouldn't they rather be normalized to
> zero as they are in other situations (e.g. toplevel statements), too?")
> may simply be yet another fine point that one might want to address in
> the future.
> In particular, this fine point is completely orthogonal to the issue of
> concrete syntax for indexnames that was raised initially.
I have worked on all this for many years, and there are connections in
very fine points.
More information about the isabelle-dev