# HG changeset patch
# User huffman
# Date 1215788180 -7200
# Node ID d315a513a150faf75298a90e03fb0303bd246608
# Parent  15cf4ed9c2a1f0db4d97749a694218777e2272b6
instance real_field < field_char_0;
instance star :: (field_char_0) field_char_0

diff -r 15cf4ed9c2a1 -r d315a513a150 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Fri Jul 11 09:03:25 2008 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Fri Jul 11 16:56:20 2008 +0200
@@ -85,6 +85,8 @@
 
 instance star :: (real_div_algebra) real_div_algebra ..
 
+instance star :: (field_char_0) field_char_0 ..
+
 instance star :: (real_field) real_field ..
 
 lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"
diff -r 15cf4ed9c2a1 -r d315a513a150 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Jul 11 09:03:25 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Fri Jul 11 16:56:20 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 *}