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...
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and