--- a/src/HOL/Num.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Num.thy Wed Feb 17 21:51:57 2016 +0100
@@ -833,6 +833,11 @@
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>
\<close>
@@ -1099,6 +1104,8 @@
context linordered_field
begin
+subclass field_char_0 ..
+
lemma half_gt_zero_iff:
"0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
by (auto simp add: field_simps)