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