src/HOL/Num.thy
changeset 62481 b5d8e57826df
parent 62348 9a5f43dac883
child 62597 b3f2b8c906a6
--- 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>