re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef

--- a/src/HOL/Real/RealVector.thy	Fri Jul 11 09:03:11 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Fri Jul 11 09:03:25 2008 +0200
@@ -1,6 +1,6 @@
-(*  Title       : RealVector.thy
+(*  Title:      RealVector.thy
     ID:         $Id$
-    Author      : Brian Huffman
+    Author:     Brian Huffman
 *)
 
 header {* Vector Spaces and Algebras over the Reals *}
@@ -261,8 +261,6 @@
     by (simp only: of_real_of_nat_eq)
 qed
 
-instance real_field < field_char_0 ..
-
 
 subsection {* The Set of Real Numbers *}