src/HOL/RealVector.thy

--- a/src/HOL/RealVector.thy	Mon Apr 26 11:34:15 2010 +0200
+++ b/src/HOL/RealVector.thy	Mon Apr 26 11:34:17 2010 +0200
@@ -207,7 +207,7 @@
 by (rule inverse_unique, simp)
 
 lemma inverse_scaleR_distrib:
-  fixes x :: "'a::{real_div_algebra,division_by_zero}"
+  fixes x :: "'a::{real_div_algebra,division_ring_inverse_zero}"
   shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
 apply (case_tac "a = 0", simp)
 apply (case_tac "x = 0", simp)
@@ -250,7 +250,7 @@
 
 lemma of_real_inverse [simp]:
   "of_real (inverse x) =
-   inverse (of_real x :: 'a::{real_div_algebra,division_by_zero})"
+   inverse (of_real x :: 'a::{real_div_algebra,division_ring_inverse_zero})"
 by (simp add: of_real_def inverse_scaleR_distrib)
 
 lemma nonzero_of_real_divide:
@@ -260,7 +260,7 @@
 
 lemma of_real_divide [simp]:
   "of_real (x / y) =
-   (of_real x / of_real y :: 'a::{real_field,division_by_zero})"
+   (of_real x / of_real y :: 'a::{real_field,division_ring_inverse_zero})"
 by (simp add: divide_inverse)
 
 lemma of_real_power [simp]:
@@ -370,7 +370,7 @@
 done
 
 lemma Reals_inverse [simp]:
-  fixes a :: "'a::{real_div_algebra,division_by_zero}"
+  fixes a :: "'a::{real_div_algebra,division_ring_inverse_zero}"
   shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
@@ -386,7 +386,7 @@
 done
 
 lemma Reals_divide [simp]:
-  fixes a b :: "'a::{real_field,division_by_zero}"
+  fixes a b :: "'a::{real_field,division_ring_inverse_zero}"
   shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
@@ -726,7 +726,7 @@
 done
 
 lemma norm_inverse:
-  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+  fixes a :: "'a::{real_normed_div_algebra,division_ring_inverse_zero}"
   shows "norm (inverse a) = inverse (norm a)"
 apply (case_tac "a = 0", simp)
 apply (erule nonzero_norm_inverse)
@@ -738,7 +738,7 @@
 by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
 
 lemma norm_divide:
-  fixes a b :: "'a::{real_normed_field,division_by_zero}"
+  fixes a b :: "'a::{real_normed_field,division_ring_inverse_zero}"
   shows "norm (a / b) = norm a / norm b"
 by (simp add: divide_inverse norm_mult norm_inverse)