--- a/src/HOL/Library/BNF_Corec.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Library/BNF_Corec.thy Thu Feb 15 12:11:00 2018 +0100
@@ -72,7 +72,7 @@
lemma self_bounded_weaken_right: "(a :: 'a :: semilattice_inf) \<le> inf b a \<Longrightarrow> a \<le> b"
by (erule le_infE)
-lemma symp_iff: "symp R \<longleftrightarrow> R = R^--1"
+lemma symp_iff: "symp R \<longleftrightarrow> R = R\<inverse>\<inverse>"
by (metis antisym conversep.cases conversep_le_swap predicate2I symp_def)
lemma equivp_inf: "\<lbrakk>equivp R; equivp S\<rbrakk> \<Longrightarrow> equivp (inf R S)"