src/HOL/HOL.thy

   (*Extensionality is built into the meta-logic, and this rule expresses
     a related property.  It is an eta-expanded version of the traditional
     rule, and similar to the ABS rule of HOL.*)
   ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
 
-  selectI:      "P (x::'a) ==> P (@x. P x)"
+  someI:        "P (x::'a) ==> P (@x. P x)"
 
   impI:         "(P ==> Q) ==> P-->Q"
   mp:           "[| P-->Q;  P |] ==> Q"
 
 defs