src/HOL/Num.thy
changeset 62348 9a5f43dac883
parent 61944 5d06ecfdb472
child 62481 b5d8e57826df
     1.1 --- a/src/HOL/Num.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Num.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -833,6 +833,11 @@
     1.4  
     1.5  end
     1.6  
     1.7 +text\<open>Also the class for fields with characteristic zero.\<close>
     1.8 +
     1.9 +class field_char_0 = field + ring_char_0
    1.10 +
    1.11 +
    1.12  subsubsection \<open>
    1.13    Structures with negation and order: class \<open>linordered_idom\<close>
    1.14  \<close>
    1.15 @@ -1099,6 +1104,8 @@
    1.16  context linordered_field
    1.17  begin
    1.18  
    1.19 +subclass field_char_0 ..
    1.20 +
    1.21  lemma half_gt_zero_iff:
    1.22    "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
    1.23    by (auto simp add: field_simps)