# HG changeset patch # User wenzelm # Date 1638799815 -3600 # Node ID fa5476c547315c6d0230c224faf30530228448bc # Parent 2df334453c4cfbfdfdf2ca63f139786dd6291357 tuned proof; diff -r 2df334453c4c -r fa5476c54731 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Mon Dec 06 12:39:59 2021 +0100 +++ b/src/HOL/BNF_Def.thy Mon Dec 06 15:10:15 2021 +0100 @@ -139,7 +139,7 @@ lemma pick_middlep: "(P OO Q) a c \ P a (pick_middlep P Q a c) \ Q (pick_middlep P Q a c) c" - unfolding pick_middlep_def apply(rule someI_ex) by auto + unfolding pick_middlep_def by (rule someI_ex) auto definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"