[isabelle-dev] NEWS

[Makarius]

On Thu, 10 Sep 2015, Larry Paulson wrote:

> Purely FYI: the names of all of these constants were originally based on 
> the corresponding names in Martin-Löf type theory.

I do remember the good old times of MLTT, where it was clear what the 
basic combinators are.

Interestingly, MLTT is up-to-date once again, in the guise of HoTT.  I now 
wonder if these guys have a 15th standard of naming things, or are using 
the primordial one.


 	Makarius