| changeset 69272 | 15e9ed5b28fb |
| parent 69064 | 5840724b1d71 |
| child 69286 | e4d5a07fecb6 |
--- a/src/HOL/Analysis/Starlike.thy Thu Nov 08 22:02:07 2018 +0100 +++ b/src/HOL/Analysis/Starlike.thy Thu Nov 08 22:29:09 2018 +0100 @@ -7957,7 +7957,7 @@ qed -subsection{*Orthogonal complement*} +subsection\<open>Orthogonal complement\<close> definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80) where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"