--- a/src/HOL/NSA/HyperDef.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Apr 26 15:37:50 2010 +0200
@@ -140,12 +140,12 @@
lemma of_hypreal_inverse [simp]:
"\<And>x. of_hypreal (inverse x) =
- inverse (of_hypreal x :: 'a::{real_div_algebra,division_ring_inverse_zero} star)"
+ inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)"
by transfer (rule of_real_inverse)
lemma of_hypreal_divide [simp]:
"\<And>x y. of_hypreal (x / y) =
- (of_hypreal x / of_hypreal y :: 'a::{real_field,division_ring_inverse_zero} star)"
+ (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)"
by transfer (rule of_real_divide)
lemma of_hypreal_eq_iff [simp]:
@@ -454,7 +454,7 @@
by transfer (rule field_power_not_zero)
lemma hyperpow_inverse:
- "\<And>r n. r \<noteq> (0::'a::{division_ring_inverse_zero,field} star)
+ "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
by transfer (rule power_inverse)