[isabelle-dev] What is this 3 levels of lambda calculi?

Makarius makarius at sketis.net
Tue Mar 3 11:50:21 CET 2015

On Tue, 3 Mar 2015, Askar Safin wrote:

> Isabelle docs says that the system contains "3 levels of lambda calculi 
> with corresponding arrows =>, !! (aka \<And>) and ==>".

This is a plain isabelle-users question, not isabelle-dev. I will consider 
writing something about it on the other mailing list, but there might be 
other experts over there.


More information about the isabelle-dev mailing list