--- a/src/HOL/Num.thy Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Num.thy Tue Mar 01 10:36:19 2016 +0100
@@ -761,7 +761,7 @@
Equality and negation: class \<open>ring_char_0\<close>
\<close>
-class ring_char_0 = ring_1 + semiring_char_0
+context ring_char_0
begin
lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
@@ -833,10 +833,6 @@
end
-text\<open>Also the class for fields with characteristic zero.\<close>
-
-class field_char_0 = field + ring_char_0
-
subsubsection \<open>
Structures with negation and order: class \<open>linordered_idom\<close>