src/HOL/Int.thy
changeset 59667 651ea265d568
parent 59613 7103019278f0
child 60162 645058aa9d6f
--- a/src/HOL/Int.thy	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/HOL/Int.thy	Tue Mar 10 15:20:40 2015 +0000
@@ -1599,4 +1599,8 @@
 lifting_update int.lifting
 lifting_forget int.lifting
 
+text{*Also the class for fields with characteristic zero.*}
+class field_char_0 = field + ring_char_0
+subclass (in linordered_field) field_char_0 ..
+
 end