[isabelle] Word vs WordMain



Hi,

I'm new to Isabelle/HOL. I'm supposed to understand a theory which
imports WordMain (and the author of the theory is still in holidays).
Here comes my first problem:

1) Where do I find WordMain.thy?

I found Word.thy in Isabelle/HOL/src/Word/
Hence here my second question:

2) What is the difference between WordMain.thy and Word.thy?

And now more specific:

3) Why does
types word32 = "32 word"
give an inner syntax error? it is the first line after "begin" in
WordExamples.thy and i thought this should work out of the box.
Where could be my mistake?

I did the first exercises of the Isabelle HOL tutorial, so the basic
part of my Isabelle system should work.

Greetings from Berlin
Nils





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