Re: [isabelle] Parsing specification for lemma

On Mon, 6 Aug 2012, Makarius wrote:

Since you are already using Isbelle/jEdit, most of the historic complications of keyword tables disappear. You just work directly in the given A.thy file.

One more thing: CTRL with mouse hovering gives you information about inferred ML types, and hyperlinks of defined ML items, which is indispensible to work with Isabelle/ML effectively -- and to learn it in the first place. (Mac users need to use COMMAND instead of CTRL.)


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