Re: [isabelle] Word vs WordMain

Hi Nils,

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 release:

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

  imports "~~/src/HOL/Word/Word"

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 -> Logics".

Hope this helps,


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