On Thu, Dec 2, 2010 at 11:26 AM, Makarius <[email protected]> wrote: > Back to history: in 2005 Brian had a paper on TPHOLs with a footnote about > an unexpected crash of the typedef package due to hidden polymorphism in the > set involved, not the type.
It was a simple error message, not a "crash". > What I did then is to make the typedef package > insert "itself" arguments in the way one would think of as a first idea. *My* first idea was that "typedef" didn't need to be defining a set constant at all. > This made the problem go away for the moment, although it complicated the > package implementation. When Larry was asking me about that change of > typedef later, I also failed to explain to him both the problem and its > solution. I'm surprised that you bothered with such a complicated solution when such a simple workaround existed -- the same workaround that I used in that paper -- just use "typedef (open)". If the default behavior of the "typedef" command was to work like "typedef (open)" (and I think it ought to be), then there would have been no problem, and no need for the footnote explaining what the "(open)" option means. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
