diff -r 516e81f75957 -r b680e74eb6f2 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Fri Jun 29 23:04:36 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy	Sat Jun 30 15:44:04 2018 +0100
@@ -333,11 +333,6 @@
     and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3))
 
-(*
-lemma (in cring) is_comm_monoid:
-  "comm_monoid R"
-  by (auto intro!: comm_monoidI m_assoc m_comm)
-*)
 lemma (in cring) is_cring:
   "cring R" by (rule cring_axioms)
 
@@ -652,6 +647,15 @@
 text \<open>Field would not need to be derived from domain, the properties
   for domain follow from the assumptions of field\<close>
 
+lemma fieldE :
+  fixes R (structure)
+  assumes "field R"
+  shows "cring R"
+    and one_not_zero : "\<one> \<noteq> \<zero>"
+    and integral: "\<And>a b. \<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>"
+  and field_Units: "Units R = carrier R - {\<zero>}"
+  using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all
+
 lemma (in cring) cring_fieldI:
   assumes field_Units: "Units R = carrier R - {\<zero>}"
   shows "field R"