[Matita] ng_kernel

[Enrico Tassi]

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.

Cheers
-- 
Enrico Tassi