Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy

If people want to prove theorems, they had better turn to us :-)


On 23 May 2013, at 12:17, Makarius <makarius at> wrote:

> I agree with that, although the "marketing" of proof assistants in the last 10 years or so has moved in a different direction.  Today most people think of Coq as some dependently typed functional programming language, and the Agda is emphasizing the programming aspect even more.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.