[isabelle-dev] NEWS: Isabelle sessions and build management

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Aug 3 09:05:02 CEST 2012

Am 02.08.2012 um 23:20 schrieb Makarius:

> BTW, there were other specialities in Collections, Refine_Monadic, and also Huffman concerning document generation. These were rather unexciting, and easily performed by regular system functions.

For Huffman, the "fixdoc" script is not critical. It replaces 'a with \alpha and things like that. I can live without it. But what do you mean by "regular system functions"?

Jasmin