[isabelle-dev] proper use of "error" channel

Makarius makarius at sketis.net
Tue Mar 23 12:13:55 CET 2010

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.


More information about the isabelle-dev mailing list