Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced respects2 by congruent2 because of type problem
authornipkow
Mon, 03 Jul 2006 20:03:11 +0200
changeset 19980 dc17fd6c0908
parent 19979 a0846edbe8b0
child 19981 c0f124a0d385
replaced respects2 by congruent2 because of type problem
src/HOL/Hyperreal/StarDef.thy file | annotate | diff | comparison | revisions 
--- 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))"
isabelle