[isabelle-dev] Fwd: Re: new isabelle interface

Makarius makarius at sketis.net
Mon Aug 25 13:38:43 CEST 2008


On Mon, 25 Aug 2008, Michael Nedzelsky wrote:

> > Besides what's in the source distribution, is there any internals
> > documentation I should know about?
> Yes, I want to know about it too.
> There was an attempt to document some internals: see Isabelle Documentation Project
>   http://isabelle.in.tum.de/nominal/activities/idp/
> But I do not know about any results.

Some Isabelle experts are working on that.  The idea is to instruct users 
how to produce there own Isabelle tools written in ML; things like custom 
proof methods and definitional packages.

For system builders, including UI stuff, the market share is much lower 
than regular proof tools.  The main documentation here are the sources; of 
course you can always ask about specific things on the mailing list.


	Makarius



More information about the isabelle-dev mailing list