>> It is interesting that local scopes within structured proofs generate >> theorems with nonzero indices, but of course that is a separate matter. > > Yes, that is a new aspect that was introduced around 1998/1999.
I would be more interested in the why than the when. Generating unpredictable names does not contribute to stability of proofs. Tobias _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
