changeset 59667 | 651ea265d568 |
parent 59000 | 6eb0725503fc |
child 59867 | 58043346ca64 |
--- a/src/HOL/Rat.thy Tue Mar 10 11:56:32 2015 +0100 +++ b/src/HOL/Rat.thy Tue Mar 10 15:20:40 2015 +0000 @@ -638,10 +638,6 @@ subsection {* Embedding from Rationals to other Fields *} -class field_char_0 = field + ring_char_0 - -subclass (in linordered_field) field_char_0 .. - context field_char_0 begin