Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] is it right?

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: Apr 25 2024 at 08:20 UTC