--- a/src/HOL/Hyperreal/Star.thy Mon May 14 13:24:22 2007 +0200
+++ b/src/HOL/Hyperreal/Star.thy Mon May 14 17:37:31 2007 +0200
@@ -56,9 +56,15 @@
lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
by (auto simp add: SReal_def)
+lemma STAR_star_of_Int: "*s* X Int Standard = star_of ` X"
+by (auto simp add: Standard_def)
+
lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> \<forall>y \<in> A. x \<noteq> hypreal_of_real y"
by auto
+lemma lemma_not_starA: "x \<notin> star_of ` A ==> \<forall>y \<in> A. x \<noteq> star_of y"
+by auto
+
lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
by auto