Re: [isabelle] where to add coding

Isabelle is not the best basis for adding your own code, because the underlying formal system is quite elaborate and the APIs are extensive. You haven't stated, incidentally, whether you want to extend Isabelle/HOL (and therefore higher-order logic), or another built-in logic, or Pure Isabelle (some formalism of your own).

You might consider HOL4, an implementation of higher-order logic where coding is fairly straightforward.

Larry Paulson

> On 28 Mar 2017, at 18:06, Moussa Bah <bah.demba at> wrote:
> Hi everyone,
> 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.
> many thanks,
> Moussa

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