Re: [isabelle] where to add coding

On 28/03/17 19:06, Moussa Bah wrote:

> I am new in Isabelle and I would like to implement a proposed proof
> technique in it but I don't know where I have to add my code. I am looking
> for help.

Isabelle/jEdit is a fully-featured IDE that supports development of
tools in Isabelle/ML, although most users apply it most of the time to
develop theory libraries.

To implement anything yourself, you should study how others have done
that before. E.g. pick a tool that you think is close to what you want
to do (lets say the "blast" proof method), and use C-mouse-hover-click
technique described in the Isabelle/jEdit manual to get to its
definition. This will usually lead to some ML_file or ML commands that
incorporate the new Isabelle language element.

Note that in order to browse Isabelle/ML sources of tools in
Isabelle/HOL, you need to do this with "isabelle jedit -l Pure", i.e. in
a session that does not yet contain Isabelle/HOL. In contrast, tools in
other sessions (e.g. src/HOL/Library) require the default HOL image.

It is also possible to browse Isabelle/Pure sources with full IDE
annotations by opening src/Pure/ROOT.ML in Isabelle/jEdit. Here the
level of sophistication is usually much higher than plain user-space
tools from elsewhere, but looking at the core implementation also helps
to understand how things are done properly.

Some further background information on Isabelle/ML is available in the
"implementation" manual.


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