src/HOL/Real/Hyperreal/Star.ML

--- a/src/HOL/Real/Hyperreal/Star.ML	Wed Oct 04 22:21:10 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Star.ML	Thu Oct 05 14:04:56 2000 +0200
@@ -492,6 +492,12 @@
 by (Fuf_tac 1);
 qed "inf_close_FreeUltrafilterNat_iff";
 
+Goal "inj starfun";
+by (rtac injI 1);
+by (rtac ext 1 THEN rtac ccontr 1);
+by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1);
+by (auto_tac (claset(),simpset() addsimps [starfun]));
+qed "inj_starfun";