[isabelle] thanks! the problem was resolved

Dear Dr. Lawrence Paulson and Dr. Florian Haftmann,

Yes, your suggestion was just! I found in the header of
the file OrderedGroup.ML the 8 bit characters, a umlaut (universit\"at)
and u umlaut (M\"unchen). After replacing these I succeeded in
building HOL with the current version. Many thanks!

Akira Kaneko (Dept. of Info. Sci. Ochanomizu University)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.