Re: [isabelle] Word vs WordMain
On 07/04/2010, at 3:06 AM, Nils Jähnig wrote:
> 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?
WordMain has helpfully been renamed to Word in Isabelle2009-1.
> 2) What is the difference between WordMain.thy and Word.thy
The two should be equivalent.
> 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.
I would have thought so as well.
The reason is really quite horrible considering the renaming above: if you don't build on the HOL-Word image, but rely on Isabelle loading the theory "Word" interactively, you get the wrong theory (the one in Library). If I remember correctly, this was the reason I called it WordMain in the first place.
To get the right Word theory, either
- run "isabelle make HOL-Word" in the src/HOL directory and tell ProofGeneral to use this logic (in Isabelle->Logics)
- interactively load src/HOL/Word/Word.thy and process this file before you process any of the theories that depend on it.
> Where could be my mistake?
Not really yours..
I'm not sure what I would want the fix to be, though. Another renaming of theories back to the old one (it's not that much fun to fix things back and forth) or a renaming of Library/Word or big warning letters in HOL/Word/Word.thy and WordExamples.thy?
ps: theory name spaces anyone? ;-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and