[isabelle] Word vs WordMain
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and