src/HOL/BNF_Greatest_Fixpoint.thy
changeset 61943 7fba644ed827
parent 61424 c3658c18b7bc
child 62905 52c5a25e0c96
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4  lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
     1.5    unfolding Gr_def by simp
     1.6  
     1.7 -lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
     1.8 +lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
     1.9    unfolding Gr_def by auto
    1.10  
    1.11  lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    1.12 @@ -137,7 +137,7 @@
    1.13    by (auto simp: proj_preserves)
    1.14  
    1.15  lemma relImage_relInvImage:
    1.16 -  assumes "R \<subseteq> f ` A <*> f ` A"
    1.17 +  assumes "R \<subseteq> f ` A \<times> f ` A"
    1.18    shows "relImage (relInvImage A R f) f = R"
    1.19    using assms unfolding relImage_def relInvImage_def by fast
    1.20