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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
