src/HOL/Num.thy
changeset 62481 b5d8e57826df
parent 62348 9a5f43dac883
child 62597 b3f2b8c906a6
     1.1 --- a/src/HOL/Num.thy	Tue Mar 01 10:32:55 2016 +0100
     1.2 +++ b/src/HOL/Num.thy	Tue Mar 01 10:36:19 2016 +0100
     1.3 @@ -761,7 +761,7 @@
     1.4    Equality and negation: class \<open>ring_char_0\<close>
     1.5  \<close>
     1.6  
     1.7 -class ring_char_0 = ring_1 + semiring_char_0
     1.8 +context ring_char_0
     1.9  begin
    1.10  
    1.11  lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
    1.12 @@ -833,10 +833,6 @@
    1.13  
    1.14  end
    1.15  
    1.16 -text\<open>Also the class for fields with characteristic zero.\<close>
    1.17 -
    1.18 -class field_char_0 = field + ring_char_0
    1.19 -
    1.20  
    1.21  subsubsection \<open>
    1.22    Structures with negation and order: class \<open>linordered_idom\<close>