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