--- a/src/HOL/Real/RealVector.thy Wed Jul 09 22:33:35 2008 +0200
+++ b/src/HOL/Real/RealVector.thy Thu Jul 10 07:07:54 2008 +0200
@@ -261,6 +261,8 @@
by (simp only: of_real_of_nat_eq)
qed
+instance real_field < field_char_0 ..
+
subsection {* The Set of Real Numbers *}