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