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



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





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