# HG changeset patch
# User haftmann
# Date 1215759805 -7200
# Node ID 15cf4ed9c2a1f0db4d97749a694218777e2272b6
# Parent  9a5543d4cc2405fa279d12c030870578879fe48b
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef

diff -r 9a5543d4cc24 -r 15cf4ed9c2a1 src/HOL/Real/RealVector.thy
--- 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 *}