Re: [isabelle] Quotients of nominal types

On Mon, 12 Aug 2013, Christian Urban wrote:

So we can talk about Isabelle/ML and be very grateful that it is so smoothly
integreated with everything else. But the fact remains that almost all people
who want to learn Isabelle do not want to learn anything about ML and its
poorly documented infrastructure that is called Isabelle distribution.

Using Isabelle/ML is definitely not trivial, but it is much easier than it used to be several years ago, and the official documentation is continously getting more and more complete, although rather thick now. It is also much better than Coq, for example, where the reader of the sources also needs to know some French, not just OCaml.

Getting basic terminology right is only the starting point, it is necessary but not sufficient for what follows for those Isabelle users who want to embark on building their own tools for the platform.


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