diff -r 0826b7025d07 -r f16e4fb20652 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jun 19 07:53:33 2015 +0200
+++ b/src/HOL/Divides.thy	Fri Jun 19 07:53:35 2015 +0200
@@ -22,7 +22,7 @@
     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
 begin
 
-subclass semidom_divide
+subclass algebraic_semidom
 proof
   fix b a
   assume "b \<noteq> 0"
@@ -212,18 +212,6 @@
   finally show ?thesis .
 qed
 
-lemma dvd_div_mult_self [simp]:
-  "a dvd b \<Longrightarrow> (b div a) * a = b"
-  using mod_div_equality [of b a, symmetric] by simp
-
-lemma dvd_mult_div_cancel [simp]:
-  "a dvd b \<Longrightarrow> a * (b div a) = b"
-  using dvd_div_mult_self by (simp add: ac_simps)
-
-lemma dvd_div_mult:
-  "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
-  by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
-
 lemma div_dvd_div [simp]:
   assumes "a dvd b" and "a dvd c"
   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
@@ -359,15 +347,6 @@
   apply (simp add: no_zero_divisors)
   done
 
-lemma div_mult_swap:
-  assumes "c dvd b"
-  shows "a * (b div c) = (a * b) div c"
-proof -
-  from assms have "b div c * (a div 1) = b * a div (c * 1)"
-    by (simp only: div_mult_div_if_dvd one_dvd)
-  then show ?thesis by (simp add: mult.commute)
-qed
-   
 lemma div_mult_mult2 [simp]:
   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   by (drule div_mult_mult1) (simp add: mult.commute)
@@ -1911,6 +1890,10 @@
 
 end
 
+lemma is_unit_int:
+  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
+  by auto
+
 text{*Basic laws about division and remainder*}
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"