# HG changeset patch
# User berghofe
# Date 1092652149 -7200
# Node ID fbf90acc5bf4b1fe2fc2e17ccb1541dbecdd3d9c
# Parent  da03f05815b0af51b2f562b4accf8448b491a965
Replaced `div and `mod in consts_code section by div and mod.

diff -r da03f05815b0 -r fbf90acc5bf4 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Sat Aug 14 16:27:56 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy	Mon Aug 16 12:29:09 2004 +0200
@@ -839,8 +839,8 @@
   "uminus" :: "int => int"      ("`~")
   "op +" :: "int => int => int" ("(_ `+/ _)")
   "op *" :: "int => int => int" ("(_ `*/ _)")
-  "op div" :: "int => int => int" ("(_ `div/ _)")
-  "op mod" :: "int => int => int" ("(_ `mod/ _)")
+  "op div" :: "int => int => int" ("(_ div/ _)")
+  "op mod" :: "int => int => int" ("(_ mod/ _)")
   "op <" :: "int => int => bool" ("(_ </ _)")
   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                         ("(_ < 0)")