[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Makarius]

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.


 	Makarius