src/HOL/BNF_Greatest_Fixpoint.thy
 changeset 67613 ce654b0e6d69 parent 67091 1393c2340eec child 69605 a96320074298
```     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Feb 13 14:24:50 2018 +0100
1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Feb 15 12:11:00 2018 +0100
1.3 @@ -31,7 +31,7 @@
1.4  lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
1.5    by fast
1.6
1.7 -lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
1.8 +lemma converse_Times: "(A \<times> B)\<inverse> = B \<times> A"
1.9    by fast
1.10
1.11  lemma equiv_proj:
1.12 @@ -56,7 +56,7 @@
1.13  lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
1.14    by auto
1.15
1.16 -lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
1.17 +lemma image2_Gr: "image2 A f g = (Gr A f)\<inverse> O (Gr A g)"
1.18    unfolding image2_def Gr_def by auto
1.19
1.20  lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
1.21 @@ -99,10 +99,10 @@
1.22    "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
1.23
1.24  lemma relImage_Gr:
1.25 -  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
1.26 +  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)\<inverse> O R O Gr A f"
1.27    unfolding relImage_def Gr_def relcomp_def by auto
1.28
1.29 -lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
1.30 +lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)\<inverse>"
1.31    unfolding Gr_def relcomp_def image_def relInvImage_def by auto
1.32
1.33  lemma relImage_mono:
```