# HG changeset patch
# User huffman
# Date 1126053518 -7200
# Node ID 560cf01f4772a4fa6f9e0d484312e68d1fa89aae
# Parent  25aab757672bc2c8ff2ce3b4a4b4eab70686ee77
generalized types more

diff -r 25aab757672b -r 560cf01f4772 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Wed Sep 07 02:16:03 2005 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Sep 07 02:38:38 2005 +0200
@@ -27,15 +27,15 @@
     "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
 
-    starfun :: "('a => 'a) => 'a star => 'a star"       ("*f* _" [80] 80)
+    starfun :: "('a => 'b) => 'a star => 'b star"       ("*f* _" [80] 80)
     "*f* f  == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. f(X n)}))"
 
     (* internal functions *)
-    starfun_n :: "(nat => ('a => 'a)) => 'a star => 'a star"
+    starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star"
                  ("*fn* _" [80] 80)
     "*fn* F  == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. (F n)(X n)}))"
 
-    InternalFuns :: "('a star => 'a star) set"
+    InternalFuns :: "('a star => 'b star) set"
     "InternalFuns == {X. \<exists>F. X = *fn* F}"
 
 
@@ -55,7 +55,7 @@
 
 subsection{*Properties of the Star-transform Applied to Sets of Reals*}
 
-lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
+lemma STAR_real_set: "*s*(UNIV::'a set) = (UNIV::'a star set)"
 by (simp add: starset_def)
 declare STAR_real_set [simp]