[Matita] ng_kernel

[Enrico Tassi]

On Wed, Nov 09, 2011 at 05:14:11PM -0500, roconnor at theorem.ca wrote:
> >Recent svn snapshot got rid of the "n" prefix to proof commands.
> 
> How do I use/include the ng library?

If I'm not mistaken there was just one include command, files in the
new library (called nlibrary at that time) were named differently.
try to include arithmetics/nat.ma for example

Note that at some extent you can mix the two libraries, since there are
translation functions triggered automatically. But this was mainly used
for testing, it's not the recommended way to use the tool.

Ciao
-- 
Enrico Tassi