[isabelle] div instances?



Hi, I'm trying to show that a certain type constructor is an instance of the 'div' axclass in HOL. However, Isabelle is giving me a syntax error message. Below is a short Isar script that illustrates the problem. Showing that the type constructor is an instance of the plus class works fine,

  datatype 'a lift = L 'a

  instance lift :: (plus)plus ..

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

Thanks,
-john





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