src/HOL/BNF_Def.thy
changeset 61423 9b6a0fb85fa3
parent 61422 0dfcd0fb4172
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:14 2015 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4    by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
     1.5  
     1.6  lemma csquare_fstOp_sndOp:
     1.7 -  "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
     1.8 +  "csquare (Collect (f (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
     1.9    unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
    1.10  
    1.11  lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy"