Re: [isabelle] Syntax for theory definitions

Amine Chaieb wrote:
Isabelle's documentation, including tutorials, is tested in every release and even in every development snapshot. The documentation files are generated from Isabelle, and they actually go through the Isabelle Kernel to check the proved theorems and the syntax etc...


Dear Amine,

I'm not sure precisely what your point is, but let me assure I'm not denying that for each theory file my colleague found on the web, there is a version of Isabelle in which it runs successfully.

Nor was I asserting that either or both the theory files he found was taken out of an Isabelle release.

Jeremy Dawson

PS. Anyway, what aspects of the documentation are actually tested? I notice that the Isabelle2008 documentation refers to a significant number of functions which don't seem to exist in the actual Isabelle2008 (eg, context, update_thy, byev, findI, get_thm, brs), unless they're hidden in some structure - but if that is so, the documentation should say so.

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