Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
On 11/12/16 23:17, Makarius wrote:
> We need more clarity and more honesty.
Hugo Herbelin is actually an expert an that.
Here is an example from a recent thread on coq-club "safe interface for
writing Coq plugins"
"plugin" is just an OCaml module produced by the user; in Isabelle/ML
that is trivial and does not need a special name).
That is an accurate and calm explanation of the realities of Coq,
without causing an uproar on the mailing list. Very professional.
This archive was generated by a fusion of
Pipermail (Mailman edition) and