Re: [isabelle] How do I do stone age interaction?



On Mon, 6 Dec 2010, Lawrence Paulson wrote:

For Isabelle 2005, just use the included documentation. I hope that it is reasonably complete.

You will find lots of useful “read" functions in the files sign.ML and thm.ML.

There is also a lot of confusion here, because Isabelle2005 features about 2 or 3 versions of basic things like syntax layers, goal modules etc.
The "read" function is an odd leftover from much earlier times.

If you really want to learn about "stone age" Isabelle, I recommend something like Isabelle98, or even 89. If you want to learn about current Isabelle, then use the current release Isabelle2009-2. The impracticability of using the raw ML loop in contemporay Isabelle is not accidental, but an integral part of the system. By dropping out of it, you won't learn the most important things.


	Makarius


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