Re: [isabelle] Isabelle Foundation & Certification



> 
> 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.

A leap ahead for Isabelle!

--
  Peter

p.s.
  I hope we won't find much more problems of this kind, i.e., commands
that are considered safe, but make the theory inconsistent, be it due to
an implementation bug or some documented axiomatic behaviour that most
users simply do not expect/know of.






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