Re: [isabelle] Syntax for theory definitions
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...
Jeremy Dawson wrote:
On a similar theme, I have been recently helping a colleague who wants
to get some familiarity with Isabelle. He found some tutorial material
on the web somewhere, but it didn't work. Why? Because it was written
before the changes made in Isabelle2007. We had to revert to
Isabelle2005 to run it.
Yesterday, he was trying to run a different lot of tutorial material
which he had found somewhere. It didn't work either, because it used a
form of syntax I've never seen before. I would guess it's Isabelle2008
(which I've never used). (It's primrec statement is totally different
from anything I've seen in the last 10 years).
These issues seem to be capable of causing massive and unnecessary
This archive was generated by a fusion of
Pipermail (Mailman edition) and