--- a/src/HOL/Complex/CStar.thy Wed Sep 27 16:33:08 2006 +0200
+++ b/src/HOL/Complex/CStar.thy Wed Sep 27 18:34:26 2006 +0200
@@ -12,12 +12,9 @@
subsection{*Properties of the *-Transform Applied to Sets of Reals*}
-lemma STARC_SComplex_subset: "SComplex \<subseteq> *s* (UNIV:: complex set)"
-by simp
-
lemma STARC_hcomplex_of_complex_Int:
"*s* X Int SComplex = hcomplex_of_complex ` X"
-by (auto simp add: SComplex_def STAR_mem_iff)
+by (auto simp add: SComplex_def)
lemma lemma_not_hcomplexA:
"x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
@@ -25,13 +22,6 @@
subsection{*Theorems about Nonstandard Extensions of Functions*}
-lemma cstarfun_if_eq:
- "w \<noteq> hcomplex_of_complex x
- ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w"
-apply (cases w)
-apply (simp add: star_of_def starfun star_n_eq_iff, ultra)
-done
-
lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
apply (cases Z)
apply (simp add: hcpow starfun hypnat_of_nat_eq)
@@ -69,8 +59,4 @@
apply (simp add: starfun hIm hRe approx_approx_iff)
done
-lemma starfunC_Idfun_approx:
- "x @= hcomplex_of_complex a ==> ( *f* (%x. x)) x @= hcomplex_of_complex a"
-by simp
-
end