Re: [isabelle] div instances?

Thanks Stefan, that did the trick.


On Feb 13, 2006, at 10:20 AM, Stefan Berghofer wrote:

John Matthews wrote:
but when I give Isar this command,
  instance lift :: (div)div ..
Isabelle responds with this syntax error message:
  *** Inner syntax error at: "div"
  *** Expected tokens:  "{" "{}" "longid" "id"
  *** At command "instance".

It seems that the Isabelle parser confuses the infix "div" operator
with the "div" type class. To circumvent this problem, you can prefix
"div" with the name of the theory "Divides" in which it is declared, i.e.

instance lift :: (Divides.div)Divides.div ..


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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