[isabelle-dev] NEWS

Makarius makarius at sketis.net
Thu Sep 10 17:06:50 CEST 2015

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.


More information about the isabelle-dev mailing list