On Tue, 23 Mar 2010, Tobias Nipkow wrote:
Makarius schrieb:
A few hints on using the "error" function in Isabelle/ML properly.
Shouldn't this go into some documentation for future reference?
I have marked it as one of the items to go into the chapter 0 about
Isabelle/ML of the Isabelle/Isar implementation manual. That part is
still to be written, or rather assembled from parts of older manuals. In
my last vacation I was pretty close to continue there, but in the end the
vacation turned out too short.
Nonetheless I did manage to update some other parts about about basic
context management, although in the process I was surprised how many of
the things that I usually say to people personally are already in there.
This indicates that our general manual situation is probably too complex
for people to actually look there.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
