# HG changeset patch
# User kuncar
# Date 1377209540 -7200
# Node ID fbf4d50dec91a48dea97a7d6dc710186e347eea5
# Parent  5565d1b56f84f0663669c2e5a15b68e9b6305674
remove OP

diff -r 5565d1b56f84 -r fbf4d50dec91 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Aug 22 23:03:23 2013 +0200
+++ b/src/HOL/Lifting.thy	Fri Aug 23 00:12:20 2013 +0200
@@ -576,13 +576,13 @@
 using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
 by (fast intro: fun_eq_iff)
 
-definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"  (infixr "OP" 75)
+definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
 where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y"
 
 lemma pcr_Domainp:
 assumes "Domainp B = P"
-shows "Domainp (A OO B) = (A OP P)"
-using assms unfolding rel_pred_comp_def by blast
+shows "Domainp (A OO B) = (\<lambda>x. \<exists>y. A x y \<and> P y)"
+using assms by blast
 
 lemma pcr_Domainp_total:
   assumes "bi_total B"