src/HOL/Integ/NatBin.thy
changeset 15129 fbf90acc5bf4
parent 15013 34264f5e4691
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Integ/NatBin.thy	Sat Aug 14 16:27:56 2004 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Aug 16 12:29:09 2004 +0200
     1.3 @@ -839,8 +839,8 @@
     1.4    "uminus" :: "int => int"      ("`~")
     1.5    "op +" :: "int => int => int" ("(_ `+/ _)")
     1.6    "op *" :: "int => int => int" ("(_ `*/ _)")
     1.7 -  "op div" :: "int => int => int" ("(_ `div/ _)")
     1.8 -  "op mod" :: "int => int => int" ("(_ `mod/ _)")
     1.9 +  "op div" :: "int => int => int" ("(_ div/ _)")
    1.10 +  "op mod" :: "int => int => int" ("(_ mod/ _)")
    1.11    "op <" :: "int => int => bool" ("(_ </ _)")
    1.12    "op <=" :: "int => int => bool" ("(_ <=/ _)")
    1.13    "neg"                         ("(_ < 0)")