# HG changeset patch
# User huffman
# Date 1215666474 -7200
# Node ID 13137fcd49aa94c4b23a06c914fb22bb9e5bbf3a
# Parent  6fcf6864d703f684e11df2b18d8cf42e21104efc
instance real_field < field_char_0

diff -r 6fcf6864d703 -r 13137fcd49aa src/HOL/Real/RealVector.thy
--- 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 *}