[isabelle-dev] Explanation required

[Christian Sternagel]

Dear all,

please forgive my annoying questioning. Could anybody elaborate on the 
following comment (to be found in HOL.thy):

   ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
   -- {*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*}

How is extensionality already part of the meta-logic (and how could it 
be applied, e.g., in Isabelle/ML)? And why is "ext" needed? Shouldn't 
this be derivable if we have extensionality?

I know that I read about this in some HOL book, but I forgot in which 
one. Maybe someone could clarify also the following:

For me, extensionality in the meta-logic would be something like "(!!x. 
f x == g x) ==> f == g", i.e., (almost) the eta-contracted variant of 
"ext" above. Is the eta-expanded version (i.e., ext) merely convenient 
or really needed?

cheers

chris