diff -r 5cdf3903a302 -r d46de31a50c4 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
@@ -415,6 +415,33 @@
 
 end
 
+class divide =
+  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+context semiring
+begin
+
+lemma [field_simps]:
+  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+  by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+  by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+  
 class semiring_no_zero_divisors = semiring_0 +
   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 begin