src/HOL/Integ/NatBin.thy

   "0" :: "int"                  ("0")
   "1" :: "int"                  ("1")
   "uminus" :: "int => int"      ("`~")
   "op +" :: "int => int => int" ("(_ `+/ _)")
   "op *" :: "int => int => int" ("(_ `*/ _)")
+(* Fails for 0:
   "op div" :: "int => int => int" ("(_ div/ _)")
   "op mod" :: "int => int => int" ("(_ mod/ _)")
+*)
   "op <" :: "int => int => bool" ("(_ </ _)")
   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                         ("(_ < 0)")
 
 ML {*