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

Amine.

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

Jeremy








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