src/HOL/Hyperreal/HyperDef.thy

--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Sep 19 05:54:17 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Sep 19 06:22:26 2006 +0200
@@ -65,6 +65,10 @@
 
 instance star :: (real_algebra_1) real_algebra_1 ..
 
+instance star :: (real_div_algebra) real_div_algebra ..
+
+instance star :: (real_field) real_field ..
+
 lemma star_of_real_def [transfer_unfold]: "of_real r \<equiv> star_of (of_real r)"
 by (rule eq_reflection, unfold of_real_def, transfer, rule refl)