Re: [isabelle] IsarMathLib
> Can I use "IsarMathLib" library in Isabelle? and where I can put this
> library file to work correctly with Isabelle commands like nitpick and
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and