# HG changeset patch
# User nipkow
# Date 1151949791 -7200
# Node ID dc17fd6c09087c1e6b66bd8a93341b6293defb1a
# Parent  a0846edbe8b0b119eaf44ef567fff6611ed4bebf
replaced respects2 by congruent2 because of type problem

diff -r a0846edbe8b0 -r dc17fd6c0908 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Mon Jul 03 20:02:42 2006 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy	Mon Jul 03 20:03:11 2006 +0200
@@ -176,7 +176,7 @@
        (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
 
 lemma Ifun_congruent2:
-  "(\<lambda>F X. starrel``{\<lambda>n. F n (X n)}) respects2 starrel"
+  "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
 by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
 
 lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"