Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange behaviour. Errors depend on file length.

view this post on Zulip Email Gateway (Aug 18 2022 at 18:04):

From: Andrzej Mazurkiewicz <andrzej@mazurkiewicz.org>
Hello everybody.

Enclosed please find two files: Example1.thy and Example2.thy.

The Example1.thy produces the following error:

*** Outer syntax error (line 55 of
"/home/andrzej/ALMAMER/PUBLIKACJE/DESIGN_PATTERNS/Isabelle/Example1.thy"):
command expected,
*** but identifier type_synonim (line 55 of
"/home/andrzej/ALMAMER/PUBLIKACJE/DESIGN_PATTERNS/Isabelle/Example1.thy") was
found

just before the following lines

definition moment_eq :: "[Moment, Moment] => bool" where
"(moment_eq x y) == (Rep_Moment x = Rep_Moment y)"

The Example2.thy file is processed without errors.

The Example2.thy is the Example1.thy with a number of lines deleted. It can be
easily checked with (on linux):
diff Example2.thy Example1.thy

Sorry for bothering you but I really do not understand the behavior.

I use linux computer with 64 bit kubuntu distribution with 1GB ram and 1GB
swap. 64 bit OpenSuse 11.3 with 8GB ram gives identical results.

Thanks for help.
Regards
Andrzej Mazurkiewicz

view this post on Zulip Email Gateway (Aug 18 2022 at 18:04):

From: Andrzej Mazurkiewicz <andrzej@mazurkiewicz.org>
Hello everybody.

Enclosed please find two files: Example1.thy and Example2.thy.

The Example1.thy produces the following error:

*** Outer syntax error (line 55 of
"/home/andrzej/ALMAMER/PUBLIKACJE/DESIGN_PATTERNS/Isabelle/Example1.thy"):
command expected,
*** but identifier type_synonim (line 55 of
"/home/andrzej/ALMAMER/PUBLIKACJE/DESIGN_PATTERNS/Isabelle/Example1.thy") was
found

just before the following lines

definition moment_eq :: "[Moment, Moment] => bool" where
"(moment_eq x y) == (Rep_Moment x = Rep_Moment y)"

The Example2.thy file is processed without errors.

The Example2.thy is the Example1.thy with a number of lines deleted. It can be
easily checked with (on linux):
diff Example2.thy Example1.thy

Sorry for bothering you but I really do not understand the behavior.

I use linux computer with 64 bit kubuntu distribution with 1GB ram and 1GB
swap. 64 bit OpenSuse 11.3 with 8GB ram gives identical results.

Thanks for help.
Regards
Andrzej Mazurkiewicz
Example1.thy
Example2.thy

view this post on Zulip Email Gateway (Aug 18 2022 at 18:04):

From: Lawrence Paulson <lp15@cam.ac.uk>
try type_synonym!

Larry Paulson

view this post on Zulip Email Gateway (Aug 18 2022 at 18:04):

From: Andrzej Mazurkiewicz <andrzej@mazurkiewicz.org>
Dnia sobota, 9 lipca 2011 o 17:28:35 Lawrence Paulson napisał(a):

try type_synonym!

Thank you for help.

Sorry for stupid error.

Regards
Andrzej Mazurkiewicz

Last updated: Apr 19 2024 at 20:15 UTC