Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof;
authorwenzelm
Mon, 06 Dec 2021 15:10:15 +0100
changeset 74886 fa5476c54731
parent 74885 2df334453c4c
child 74887 56247fdb8bbb
tuned proof;
src/HOL/BNF_Def.thy file | annotate | diff | comparison | revisions 
--- 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 \<Longrightarrow> P a (pick_middlep P Q a c) \<and> 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))"
isabelle