[Matita] ng_kernel

[roconnor at theorem.ca]

On Wed, 9 Nov 2011, Enrico Tassi wrote:

> On Wed, Nov 09, 2011 at 04:04:22PM -0500, roconnor at theorem.ca wrote:
>> Do I undrestand correctly that the kernel described in "A compact
>> kernel for the calculus of inductive constructions" is the kernel
>> used in Matita 0.5.8 (the latest release)?
>
> It actually cohexists with the old one. IIRC in that version you can
> use "ntheorem", "napply" and so on to state, proove and type check with
> the ng_kernel and ng_refiner.
>
> Recent svn snapshot got rid of the "n" prefix to proof commands.

How do I use/include the ng library?

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''