Re: [isabelle] Isabelle Foundation & Certification

On Sat, 26 Sep 2015, Peter Lammich wrote:

This may still require more polishing before the winter release of
Isabelle2016, but there is time for that.

Now Isabelle has a feature, which is (IMHO) essential for a theorem prover, and which many users (including me) deemed already present in older Isabelle's, and were surprised that it wasn't.

Now we are back to the actual social problems: Why do Isabelle power users have an inadequate idea what the system does and what not, despite the official documentation.

We need to work harder on this thread, to move forward.


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