Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] thanks! the problem was resolved

view this post on Zulip Email Gateway (Aug 17 2022 at 14:43):

From: Akira KANEKO <kanenko@atom.is.ocha.ac.jp>
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)

Last updated: Nov 21 2024 at 12:39 UTC