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 :-)

Larry

On 23 May 2013, at 12:17, Makarius <makarius at sketis.net> 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.