Re: [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?
2) What is the difference between WordMain.thy and Word.thy?
I suspect that the theory you are working with was built with Isabelle
2008. WordMain.thy was renamed to Word.thy between the 2008 and the 2009
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?
When you open WordExamples.thy with the normal HOL image loaded, then
Isabelle picks "Library/Word.thy" by default when you say "imports
Word". This is another, incompatible, development.
You can either manually adapt the import and write
or your built the HOL-Word image, which contains HOL and the Word
library. To do this, go to ~~/src/HOL where ~~ is your Isabelle
installation path, and run
isabelle make HOL-Word
After that you can select the image in Proof General under "Isabelle ->
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and