# HG changeset patch
# User haftmann
# Date 1163805622 -3600
# Node ID 39f98c88f88a6e5cf88919f46fad9cfb59bd0a37
# Parent  4cb808163adc7f902ec9106a0d394cb25cb3a2d2
op div/op mod now named without leading op

diff -r 4cb808163adc -r 39f98c88f88a src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sat Nov 18 00:20:21 2006 +0100
+++ b/src/HOL/arith_data.ML	Sat Nov 18 00:20:22 2006 +0100
@@ -460,8 +460,8 @@
                                     "HOL.abs",
                                     "HOL.minus",
                                     "IntDef.nat",
-                                    "Divides.op mod",
-                                    "Divides.op div"]
+                                    "Divides.mod",
+                                    "Divides.div"]
     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
                                  Display.string_of_thm thm);
                        false))
@@ -620,7 +620,7 @@
     (* "?P ((?n::nat) mod (number_of ?k)) =
          ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
-    | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+    | (Const ("Divides.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const ("HOL.zero", split_type)
@@ -652,7 +652,7 @@
     (* "?P ((?n::nat) div (number_of ?k)) =
          ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
-    | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+    | (Const ("Divides.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
         val zero                    = Const ("HOL.zero", split_type)
@@ -687,7 +687,7 @@
             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
           (neg (number_of ?k) -->
             (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
-    | (Const ("Divides.op mod",
+    | (Const ("Divides.mod",
         Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms
@@ -739,7 +739,7 @@
             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
           (neg (number_of ?k) -->
             (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
-    | (Const ("Divides.op div",
+    | (Const ("Divides.div",
         Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
       let
         val rev_terms               = rev terms