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.


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