# HG changeset patch
# User huffman
# Date 1158801471 -7200
# Node ID 24cda2c5fd40d30a034b49be42b3628c959915ba
# Parent  6e9b7617c89a537fa25943651fef11a22a8f9fba
removed division_by_zero class requirements from several lemmas

diff -r 6e9b7617c89a -r 24cda2c5fd40 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 21 03:16:50 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Sep 21 03:17:51 2006 +0200
@@ -330,7 +330,7 @@
 
 
 lemma NSLIM_inverse:
-  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
+  fixes L :: "'a::real_normed_div_algebra"
   shows "[| f -- a --NS> L;  L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
 apply (simp add: NSLIM_def, clarify)
@@ -339,7 +339,7 @@
 done
 
 lemma LIM_inverse:
-  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
+  fixes L :: "'a::real_normed_div_algebra"
   shows "[| f -- a --> L; L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --> (inverse L)"
 by (simp add: LIM_NSLIM_iff NSLIM_inverse)
@@ -514,16 +514,14 @@
 by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
 
 lemma isCont_inverse:
-  fixes f :: "'a::real_normed_vector \<Rightarrow>
-              'b::{real_normed_div_algebra,division_by_zero}"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
 apply (simp add: isCont_def)
 apply (blast intro: LIM_inverse)
 done
 
 lemma isNSCont_inverse:
-  fixes f :: "'a::real_normed_vector \<Rightarrow>
-              'b::{real_normed_div_algebra,division_by_zero}"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
 
diff -r 6e9b7617c89a -r 24cda2c5fd40 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Thu Sep 21 03:16:50 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Thu Sep 21 03:17:51 2006 +0200
@@ -264,25 +264,25 @@
 
 text{*Proof is like that of @{text NSLIM_inverse}.*}
 lemma NSLIMSEQ_inverse:
-  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+  fixes a :: "'a::real_normed_div_algebra"
   shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
 by (simp add: NSLIMSEQ_def star_of_approx_inverse)
 
 
 text{*Standard version of theorem*}
 lemma LIMSEQ_inverse:
-  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+  fixes a :: "'a::real_normed_div_algebra"
   shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
 by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
 
 lemma NSLIMSEQ_mult_inverse:
-  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
+  fixes a b :: "'a::{real_normed_div_algebra,field}"
   shows
      "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
 
 lemma LIMSEQ_divide:
-  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
+  fixes a b :: "'a::{real_normed_div_algebra,field}"
   shows "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)