Re: [isabelle] IsarMathLib



Hi Omar,

> Can I use "IsarMathLib" library in Isabelle? and where I can put this
> library file to work correctly with Isabelle commands like nitpick and
> sledgehammer?

yes, you can. IsarMathLib is a library for Isabelle.

As far as I know, it uses ZF as its underlying logic. However,
Sledgehammer and Nitpick, as they are implemented in Isabelle, require
HOL as underlying logic. That means you can't use them with IsarMathLib.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.