# HG changeset patch
# User huffman
# Date 1179157051 -7200
# Node ID 9dc4f5048353bc1d5a9af574161e01ad2c7b0c03
# Parent  b81bbe2984066e3ddddab6763886b5a71cd7e8c6
new lemmas

diff -r b81bbe298406 -r 9dc4f5048353 src/HOL/Hyperreal/Star.thy
--- 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