Date: Thu, 6 Feb 92 17:02:05 EST Who introduced type-labeled lambda abstraction, i.e., the version of the lambda-operator that leads to terms of the form lambda x : sigma . Z, where sigma is a type symbol? I have the impression that this version of abstraction comes from AUTOMATH, but I'm not sure, and, even if that's right, I don't know which of the AUTOMATH people came up with it. Garrel Pottinger garrel@oracorp.com