This paper discusses the choice operator @ in HOL88. It gives an intuitive interpretation, as well as the definition, and presents proof strategies for goals that contain this operator, broken down into cases based on the number of values which satisfy the predicate argument. A working knowledge of the HOL system is assumed.