--- a/src/HOL/BNF_Greatest_Fixpoint.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Sun Dec 27 22:07:17 2015 +0100
@@ -73,7 +73,7 @@
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
unfolding Gr_def by simp
-lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
+lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
unfolding Gr_def by auto
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
@@ -137,7 +137,7 @@
by (auto simp: proj_preserves)
lemma relImage_relInvImage:
- assumes "R \<subseteq> f ` A <*> f ` A"
+ assumes "R \<subseteq> f ` A \<times> f ` A"
shows "relImage (relInvImage A R f) f = R"
using assms unfolding relImage_def relInvImage_def by fast