 Aside from the investigations of the epsilon calculus in proof theory, two applications should be mentioned. One is the use of epsilon notation in Bourbaki’s Theorie des ensembles (1958). The second, of perhaps greater current interest, is the use of the epsilon-operator in the theorem-proving systems  HOL  and  Isabelle,  where the expressive power of epsilon-terms yields significant practical advantages.