Email Gateway (Aug 18 2022 at 15:28): Email Gateway (Aug 18 2022 at 15:28):From: 许庆国 <qgxu@mail.shu.edu.cn>
Dear user:
I am running Isabelle under Cygwin 1.7.
I installed it under the instrustions form http://isabelle.in.tum.de/installation.html
the following graph is a try of mine?
who can tell me are they correct about installing?
when I press button "Next", the error message turns up.
thanks a lot!
2010-06-01
Q.G. XU
Catch5.jpg
Email Gateway (Aug 18 2022 at 15:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Q.G.,
the theory header is wrong, it should read
theory Demo1
imports Main
begin
From where did you obtain that outdated example file? The examples to
be found at http://isabelle.in.tum.de/exercises/ should be up-to-date.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:31):From: Tobias Nipkow <nipkow@in.tum.de>
You are processing a very old (at least 3 years) Isabelle file. The
syntax has changed meanwhile. Hence the error message.
Your file is from my Isabelle course. Please use the latest version:
http://isabelle.in.tum.de/coursematerial/PSV2009-1/index.html
Regards
Tobias
许庆国 schrieb:
Last updated: Nov 21 2024 at 12:39 UTC