# HG changeset patch
# User haftmann
# Date 1163805624 -3600
# Node ID f23e4e75dfd30953cdb85dabb11dfc8fa9395535
# Parent  39f98c88f88a6e5cf88919f46fad9cfb59bd0a37
dvd_def now with object equality

diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Algebra/abstract/Factor.ML
--- a/src/HOL/Algebra/abstract/Factor.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Factor.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -18,7 +18,7 @@
 by (induct_tac "factors" 1);
 (* Base case: c dvd a contradicts irred c *)
 by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
-by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
+by (blast_tac (claset() addIs [thm "dvd_trans_ring"]) 1);
 (* Induction step *)
 by (ftac (thm "factorial_prime") 1);
 by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Algebra/abstract/Ideal2.ML
--- a/src/HOL/Algebra/abstract/Ideal2.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -124,7 +124,7 @@
 Goal "ideal_of {0::'a::ring} = {0}";
 by (simp_tac (simpset() addsimps [pideal_structure]) 1);
 by (rtac subset_antisym 1);
-by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
+by (auto_tac (claset() addIs [thm "dvd_zero_left"], simpset()));
 qed "ideal_of_zero_eq";
 
 Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
@@ -149,7 +149,7 @@
 (* Ideals and divisibility *)
 
 Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
-by (auto_tac (claset() addIs [dvd_trans_ring],
+by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
   simpset() addsimps [pideal_structure]));
 qed "dvd_imp_subideal";
 
@@ -167,7 +167,7 @@
 by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
 by (etac conjE 1);
 by (dres_inst_tac [("c", "a")] subsetD 1);
-by (auto_tac (claset() addIs [dvd_trans_ring],
+by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
   simpset()));
 qed "psubideal_not_dvd";
 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Algebra/abstract/Ring2.ML
--- a/src/HOL/Algebra/abstract/Ring2.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -164,61 +164,7 @@
 
 *)
 
-(* Power *)
-
-Goal "!!a::'a::ring. a ^ 0 = 1";
-by (simp_tac (simpset() addsimps [power_def]) 1);
-qed "power_0";
-
-Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
-by (simp_tac (simpset() addsimps [power_def]) 1);
-qed "power_Suc";
-
-Addsimps [power_0, power_Suc];
-
-Goal "1 ^ n = (1::'a::ring)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "power_one";
-
-Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)";
-by (etac rev_mp 1);
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "power_zero";
-
-Addsimps [power_zero, power_one];
-
-Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
-by (induct_tac "m" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "power_mult";
-
-(* Divisibility *)
-section "Divisibility";
-
-Goalw [dvd_def] "!! a::'a::ring. a dvd 0";
-by (res_inst_tac [("x", "0")] exI 1);
-by (Simp_tac 1);
-qed "dvd_zero_right";
-
-Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0";
-by Auto_tac;
-qed "dvd_zero_left";
-
-Goalw [dvd_def] "!! a::'a::ring. a dvd a";
-by (res_inst_tac [("x", "1")] exI 1);
-by (Simp_tac 1);
-qed "dvd_refl_ring";
-
-Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
-by (Step_tac 1);
-by (res_inst_tac [("x", "k * ka")] exI 1);
-by (Asm_simp_tac 1);
-qed "dvd_trans_ring";
-
-Addsimps [dvd_zero_right, dvd_refl_ring];
+val dvd_def = thm "dvd_def'";
 
 Goalw [dvd_def]
   "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";
@@ -366,7 +312,7 @@
 section "Fields";
 
 Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";
-by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left],
+by (auto_tac (claset() addDs [thm "field_ax", thm "dvd_zero_left"],
   simpset() addsimps [thm "field_one_not_zero"]));
 qed "field_unit";
 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Nov 18 00:20:24 2006 +0100
@@ -231,4 +231,54 @@
   "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
 by (simp add: m_lcancel)
 
+lemma power_0 [simp]:
+  "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp
+
+lemma power_Suc [simp]:
+  "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp
+
+lemma power_one [simp]:
+  "1 ^ n = (1::'a::ring)" by (induct n) simp_all
+
+lemma power_zero [simp]:
+  "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
+
+lemma power_mult [simp]:
+  "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
+  by (induct m) simp_all
+
+
+section "Divisibility"
+
+lemma dvd_zero_right [simp]:
+  "(a::'a::ring) dvd 0"
+proof
+  show "0 = a * 0" by simp
+qed
+
+lemma dvd_zero_left:
+  "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
+
+lemma dvd_refl_ring [simp]:
+  "(a::'a::ring) dvd a"
+proof
+  show "a = a * 1" by simp
+qed
+
+lemma dvd_trans_ring:
+  fixes a b c :: "'a::ring"
+  assumes a_dvd_b: "a dvd b"
+  and b_dvd_c: "b dvd c"
+  shows "a dvd c"
+proof -
+  from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
+  moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
+  ultimately have "c = a * (l * j)" by simp
+  then have "\<exists>k. c = a * k" ..
+  then show ?thesis using dvd_def by blast
+qed
+
+lemma dvd_def':
+  "m dvd n \<equiv> \<exists>k. n = m * k" unfolding dvd_def by simp
+
 end
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Nov 18 00:20:24 2006 +0100
@@ -187,8 +187,8 @@
   "-"          > "HOL.minus"      :: "[nat,nat]=>nat"
   MIN          > Orderings.min    :: "[nat,nat]=>nat"
   MAX          > Orderings.max    :: "[nat,nat]=>nat"
-  DIV          > "Divides.op div" :: "[nat,nat]=>nat"
-  MOD          > "Divides.op mod" :: "[nat,nat]=>nat"
+  DIV          > "Divides.div" :: "[nat,nat]=>nat"
+  MOD          > "Divides.mod" :: "[nat,nat]=>nat"
   EXP          > Nat.power        :: "[nat,nat]=>nat";
 
 end_import;
@@ -208,7 +208,7 @@
 import_theory divides;
 
 const_maps
-    divides > "Divides.op dvd" :: "[nat,nat]=>bool";
+    divides > "Divides.dvd" :: "[nat,nat]=>bool";
 
 end_import;
 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp	Sat Nov 18 00:20:24 2006 +0100
@@ -14,12 +14,12 @@
   "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
   "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
   "NUMERAL" > "HOL4Compat.NUMERAL"
-  "MOD" > "Divides.op mod" :: "nat => nat => nat"
+  "MOD" > "Divides.mod" :: "nat => nat => nat"
   "MIN" > "Orderings.min" :: "nat => nat => nat"
   "MAX" > "Orderings.max" :: "nat => nat => nat"
   "FUNPOW" > "HOL4Compat.FUNPOW"
   "EXP" > "Nat.power" :: "nat => nat => nat"
-  "DIV" > "Divides.op div" :: "nat => nat => nat"
+  "DIV" > "Divides.div" :: "nat => nat => nat"
   "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
   ">=" > "HOL4Compat.nat_ge"
   ">" > "HOL4Compat.nat_gt"
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Import/HOL/divides.imp
--- a/src/HOL/Import/HOL/divides.imp	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Import/HOL/divides.imp	Sat Nov 18 00:20:24 2006 +0100
@@ -3,7 +3,7 @@
 import_segment "hol4"
 
 const_maps
-  "divides" > "Divides.op dvd" :: "nat => nat => bool"
+  "divides" > "Divides.dvd" :: "nat => nat => bool"
 
 thm_maps
   "divides_def" > "HOL4Compat.divides_def"
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/IntDiv_setup.ML
--- a/src/HOL/Integ/IntDiv_setup.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/IntDiv_setup.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -10,8 +10,8 @@
 structure CancelDivModData =
 struct
 
-val div_name = "Divides.op div";
-val mod_name = "Divides.op mod";
+val div_name = "Divides.div";
+val mod_name = "Divides.mod";
 val mk_binop = HOLogic.mk_binop;
 val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
 val dest_sum = Int_Numeral_Simprocs.dest_sum;
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -203,10 +203,10 @@
  
 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
  
-fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
+fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
     if is_numeral c then   
       let val c' = (mk_numeral(abs(dest_numeral c)))  
-      in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) 
+      in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
       ;raise COOPER)
@@ -283,7 +283,7 @@
      let val xp = (HOLogic.mk_binop "HOL.plus"  
      		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
 	in 
-      HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
+      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
       end 
   end; 
  
@@ -354,7 +354,7 @@
 (* The LCM of all the divisors that involve x.                               *) 
 (* ------------------------------------------------------------------------- *) 
  
-fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
         if x = y then abs(dest_numeral d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
@@ -450,7 +450,7 @@
 val operations = 
   [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) , 
    ("op >=",IntInf.>=), 
-   ("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
+   ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
  
 fun applyoperation (SOME f) (a,b) = f (a, b) 
     |applyoperation _ (_, _) = false; 
@@ -460,7 +460,7 @@
 (*
 fun evalc_atom at = case at of  
   (Const (p,_) $ s $ t) =>
-   (if p="Divides.op dvd" then 
+   (if p="Divides.dvd" then 
      ((if dvd_op(s,t) then HOLogic.true_const
      else HOLogic.false_const)
       handle _ => at)
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/cooper_proof.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -300,7 +300,7 @@
 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
              end
 
-             |"Divides.op dvd" =>
+             |"Divides.dvd" =>
 	       let val pre = prove_elementar sg "lf" 
 	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
                    val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
@@ -346,16 +346,16 @@
 	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -384,7 +384,7 @@
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
@@ -392,7 +392,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -444,16 +444,16 @@
 	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -483,7 +483,7 @@
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
@@ -491,7 +491,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -595,18 +595,18 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -685,18 +685,18 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -772,7 +772,7 @@
    |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
-   |(Const("Divides.op dvd",_)$d$r) => 
+   |(Const("Divides.dvd",_)$d$r) => 
      if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
      else (warning "Nonlinear Term --- Non numeral leftside at dvd";
        raise COOPER)
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -64,8 +64,8 @@
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.op div"
-  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
+  val mk_bal   = HOLogic.mk_binop "Divides.div"
+  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
   val cancel = int_mult_div_cancel1 RS trans
   val neg_exchanges = false
 )
@@ -272,8 +272,8 @@
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.op div"
-  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
+  val mk_bal   = HOLogic.mk_binop "Divides.div"
+  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
 );
 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -294,8 +294,8 @@
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.op div"
-  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop "Divides.div"
+  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
   val cancel = nat_mult_div_cancel1 RS trans
   val neg_exchanges = false
 )
@@ -404,8 +404,8 @@
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "Divides.op div"
-  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
+  val mk_bal   = HOLogic.mk_binop "Divides.div"
+  val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
 );
 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/presburger.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -135,9 +135,9 @@
    ("Orderings.less_eq", iT --> iT --> bT),
    ("op =", iT --> iT --> bT),
    ("Orderings.less", iT --> iT --> bT),
-   ("Divides.op dvd", iT --> iT --> bT),
-   ("Divides.op div", iT --> iT --> iT),
-   ("Divides.op mod", iT --> iT --> iT),
+   ("Divides.dvd", iT --> iT --> bT),
+   ("Divides.div", iT --> iT --> iT),
+   ("Divides.mod", iT --> iT --> iT),
    ("HOL.plus", iT --> iT --> iT),
    ("HOL.minus", iT --> iT --> iT),
    ("HOL.times", iT --> iT --> iT), 
@@ -149,9 +149,9 @@
    ("Orderings.less_eq", nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
    ("Orderings.less", nT --> nT --> bT),
-   ("Divides.op dvd", nT --> nT --> bT),
-   ("Divides.op div", nT --> nT --> nT),
-   ("Divides.op mod", nT --> nT --> nT),
+   ("Divides.dvd", nT --> nT --> bT),
+   ("Divides.div", nT --> nT --> nT),
+   ("Divides.mod", nT --> nT --> nT),
    ("HOL.plus", nT --> nT --> nT),
    ("HOL.minus", nT --> nT --> nT),
    ("HOL.times", nT --> nT --> nT), 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Integ/reflected_cooper.ML
--- a/src/HOL/Integ/reflected_cooper.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -31,7 +31,7 @@
       | Const("False",_) => F
       | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
       | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Divides.op dvd",_)$t1$t2 => 
+      | Const ("Divides.dvd",_)$t1$t2 => 
 	Divides(i_of_term vs t1,i_of_term vs t2)
       | Const("op =",eqT)$t1$t2 => 
 	if (domain_type eqT = HOLogic.intT)
@@ -99,7 +99,7 @@
 			  (term_of_i vs t2)$(term_of_i vs t1)
       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Divides(t1,t2) => Const("Divides.op dvd",[iT,iT] ---> bT)$
+      | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$
 			       (term_of_i vs t1)$(term_of_i vs t2)
       | NOT t' => HOLogic.Not$(term_of_qf vs t')
       | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2)
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -203,10 +203,10 @@
  
 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
  
-fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
+fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
     if is_numeral c then   
       let val c' = (mk_numeral(abs(dest_numeral c)))  
-      in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) 
+      in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) 
       end 
     else (warning "Nonlinear term --- Non numeral leftside at dvd"
       ;raise COOPER)
@@ -283,7 +283,7 @@
      let val xp = (HOLogic.mk_binop "HOL.plus"  
      		((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
 	in 
-      HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
+      HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) 
       end 
   end; 
  
@@ -354,7 +354,7 @@
 (* The LCM of all the divisors that involve x.                               *) 
 (* ------------------------------------------------------------------------- *) 
  
-fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =  
         if x = y then abs(dest_numeral d) else 1 
   |divlcm x ( Const ("Not", _) $ p) = divlcm x p 
   |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) 
@@ -450,7 +450,7 @@
 val operations = 
   [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) , 
    ("op >=",IntInf.>=), 
-   ("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
+   ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
  
 fun applyoperation (SOME f) (a,b) = f (a, b) 
     |applyoperation _ (_, _) = false; 
@@ -460,7 +460,7 @@
 (*
 fun evalc_atom at = case at of  
   (Const (p,_) $ s $ t) =>
-   (if p="Divides.op dvd" then 
+   (if p="Divides.dvd" then 
      ((if dvd_op(s,t) then HOLogic.true_const
      else HOLogic.false_const)
       handle _ => at)
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -300,7 +300,7 @@
 	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
              end
 
-             |"Divides.op dvd" =>
+             |"Divides.dvd" =>
 	       let val pre = prove_elementar sg "lf" 
 	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
                    val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
@@ -346,16 +346,16 @@
 	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -384,7 +384,7 @@
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
@@ -392,7 +392,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -444,16 +444,16 @@
 	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
 	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
-      |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+      |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
       c $ y ) $ z))) => 
          if y=x then  let val cz = cterm_of sg (norm_zero_one z)
-			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
 	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
 		      end
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -483,7 +483,7 @@
             if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
 	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
 	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
-      |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
@@ -491,7 +491,7 @@
 
 		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
 		
-      |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+      |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
          if y=x then  let val cd = cterm_of sg (norm_zero_one d)
 	 		  val cz = cterm_of sg (norm_zero_one z)
 	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -595,18 +595,18 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -685,18 +685,18 @@
 	      end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
       if y=x then  
            let val cz = cterm_of sg (norm_zero_one z)
-	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	     in (instantiate' []  [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
 	     end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
 
-   |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
+   |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => 
        if y=x then  
 	 let val cz = cterm_of sg (norm_zero_one z)
-	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
  	    in (instantiate' []  [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
 	  end
       else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -772,7 +772,7 @@
    |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
-   |(Const("Divides.op dvd",_)$d$r) => 
+   |(Const("Divides.dvd",_)$d$r) => 
      if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
      else (warning "Nonlinear Term --- Non numeral leftside at dvd";
        raise COOPER)
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -135,9 +135,9 @@
    ("Orderings.less_eq", iT --> iT --> bT),
    ("op =", iT --> iT --> bT),
    ("Orderings.less", iT --> iT --> bT),
-   ("Divides.op dvd", iT --> iT --> bT),
-   ("Divides.op div", iT --> iT --> iT),
-   ("Divides.op mod", iT --> iT --> iT),
+   ("Divides.dvd", iT --> iT --> bT),
+   ("Divides.div", iT --> iT --> iT),
+   ("Divides.mod", iT --> iT --> iT),
    ("HOL.plus", iT --> iT --> iT),
    ("HOL.minus", iT --> iT --> iT),
    ("HOL.times", iT --> iT --> iT), 
@@ -149,9 +149,9 @@
    ("Orderings.less_eq", nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
    ("Orderings.less", nT --> nT --> bT),
-   ("Divides.op dvd", nT --> nT --> bT),
-   ("Divides.op div", nT --> nT --> nT),
-   ("Divides.op mod", nT --> nT --> nT),
+   ("Divides.dvd", nT --> nT --> bT),
+   ("Divides.div", nT --> nT --> nT),
+   ("Divides.mod", nT --> nT --> nT),
    ("HOL.plus", nT --> nT --> nT),
    ("HOL.minus", nT --> nT --> nT),
    ("HOL.times", nT --> nT --> nT), 
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Tools/Presburger/reflected_cooper.ML
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -31,7 +31,7 @@
       | Const("False",_) => F
       | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
       | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
-      | Const ("Divides.op dvd",_)$t1$t2 => 
+      | Const ("Divides.dvd",_)$t1$t2 => 
 	Divides(i_of_term vs t1,i_of_term vs t2)
       | Const("op =",eqT)$t1$t2 => 
 	if (domain_type eqT = HOLogic.intT)
@@ -99,7 +99,7 @@
 			  (term_of_i vs t2)$(term_of_i vs t1)
       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Divides(t1,t2) => Const("Divides.op dvd",[iT,iT] ---> bT)$
+      | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$
 			       (term_of_i vs t1)$(term_of_i vs t2)
       | NOT t' => HOLogic.Not$(term_of_qf vs t')
       | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2)
diff -r 39f98c88f88a -r f23e4e75dfd3 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Sat Nov 18 00:20:24 2006 +0100
@@ -117,7 +117,7 @@
 		   ("HOL.plus", "plus"),
 		   ("HOL.minus", "minus"),
 		   ("HOL.times", "times"),
-		   ("Divides.op div", "div"),
+		   ("Divides.div", "div"),
 		   ("HOL.divide", "divide"),
 		   ("op -->", "implies"),
 		   ("{}", "emptyset"),