# HG changeset patch
# User huffman
# Date 1165894370 -3600
# Node ID d75108a9665ab03d0f9d5d687a7ecf1325772df3
# Parent  bf055d30d3adaf3652d6e2d39a5a8bcb38a8ed85
generalize some theorems

diff -r bf055d30d3ad -r d75108a9665a src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue Dec 12 04:31:34 2006 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Tue Dec 12 04:32:50 2006 +0100
@@ -617,12 +617,14 @@
 done
 
 lemma Infinitesimal_hypreal_of_real_mult:
-     "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
-by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult])
+  fixes x :: "'a::real_normed_algebra star"
+  shows "x \<in> Infinitesimal ==> x * star_of r \<in> Infinitesimal"
+by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult])
 
 lemma Infinitesimal_hypreal_of_real_mult2:
-     "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
-by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult2])
+  fixes x :: "'a::real_normed_algebra star"
+  shows "x \<in> Infinitesimal ==> star_of r * x \<in> Infinitesimal"
+by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])
 
 
 subsection{*The Infinitely Close Relation*}
@@ -1743,9 +1745,9 @@
 
 (*used once, in Lim/NSDERIV_inverse*)
 lemma Infinitesimal_add_not_zero:
-     "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> hypreal_of_real x + h \<noteq> 0"
+     "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> star_of x + h \<noteq> 0"
 apply auto
-apply (subgoal_tac "h = - hypreal_of_real x", auto)
+apply (subgoal_tac "h = - star_of x", auto intro: equals_zero_I [symmetric])
 done
 
 lemma Infinitesimal_square_cancel [simp]: