remove OP
authorkuncar
Fri Aug 23 00:12:20 2013 +0200 (2013-08-23)
changeset 53151fbf4d50dec91
parent 53150 5565d1b56f84
child 53152 cbd3c7c48d2c
child 53160 317077e35b0e
remove OP
src/HOL/Lifting.thy
     1.1 --- a/src/HOL/Lifting.thy	Thu Aug 22 23:03:23 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Fri Aug 23 00:12:20 2013 +0200
     1.3 @@ -576,13 +576,13 @@
     1.4  using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
     1.5  by (fast intro: fun_eq_iff)
     1.6  
     1.7 -definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"  (infixr "OP" 75)
     1.8 +definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
     1.9  where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y"
    1.10  
    1.11  lemma pcr_Domainp:
    1.12  assumes "Domainp B = P"
    1.13 -shows "Domainp (A OO B) = (A OP P)"
    1.14 -using assms unfolding rel_pred_comp_def by blast
    1.15 +shows "Domainp (A OO B) = (\<lambda>x. \<exists>y. A x y \<and> P y)"
    1.16 +using assms by blast
    1.17  
    1.18  lemma pcr_Domainp_total:
    1.19    assumes "bi_total B"