On Wed, 22 Dec 2010 05:12:46 Victor Porton wrote: > What is "op"? This word is not defined anywhere in locales.pdf. I did a quick search in tutorial.pdf (from Isabelle 2009-2) for "op" as a whole word. The first instance I found (near the top of page 54) gave me the answer, which I suggest you look up for yourself; if I quote it here, I'm afraid I might leave out some surrounding material that would help you understand it better. Timothy <><
Description: This is a digitally signed message part.